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