1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
\DOC term_union
\TYPE {term_union : term list -> term list -> term list}
\SYNOPSIS
Union of two sets of terms up to alpha-equivalence.
\DESCRIBE
The call {term_union l1 l2} for two lists of terms {l1} and {l2} returns a list
including all of {l2} and all terms of {l1} for which no alpha-equivalent term
occurs in {l2} or earlier in {l1}. If both lists were sets modulo
alpha-conversion, i.e. contained no alpha-equivalent pairs, then so will be the
result.
\FAILURE
Never fails.
\EXAMPLE
{
# term_union [`1`; `2`] [`2`; `3`];;
val it : term list = [`1`; `2`; `3`]
# term_union [`!x. x >= 0`; `?u. u > 0`] [`?w. w > 0`; `!u. u >= 0`];;
val it : term list = [`?w. w > 0`; `!u. u >= 0`]
}
\USES
For combining assumption lists of theorems without duplication of
alpha-equivalent ones.
\SEEALSO
aconv, union, union'.
\ENDDOC
|
