1\DOC aconv
2
3\TYPE {aconv : term -> term -> bool}
4
5\SYNOPSIS
6Tests for alpha-convertibility of terms.
7
8\KEYWORDS
9alpha.
10
11\DESCRIBE
12When applied to two terms, {aconv} returns {true} if they are
13alpha-convertible, and {false} otherwise. Two terms are alpha-convertible
14if they differ only in the way that names have been given to bound variables.
15
16\FAILURE
17Never fails.
18
19\EXAMPLE
20{
21- aconv (Term `?x y. x /\ y`) (Term `?y x. y /\ x`)
22> val it = true : bool
23}
24
25
26\SEEALSO
27Thm.ALPHA, Drule.ALPHA_CONV.
28\ENDDOC
29