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 ALPHA
\TYPE {ALPHA : term -> term -> thm}
\SYNOPSIS
Proves equality of alpha-equivalent terms.
\KEYWORDS
rule, alpha.
\DESCRIBE
When applied to a pair of terms {t1} and {t1'} which are
alpha-equivalent, {ALPHA} returns the theorem {|- t1 = t1'}.
{
------------- ALPHA `t1` `t1'`
|- t1 = t1'
}
\FAILURE
Fails unless the terms provided are alpha-equivalent.
\EXAMPLE
{
# ALPHA `!x:num. x = x` `!y:num. y = y`;;
val it : thm = |- (!x. x = x) <=> (!y. y = y)
# ALPHA `\w. w + z` `\z'. z' + z`;;
val it : thm = |- (\w. w + z) = (\z'. z' + z)
}
\SEEALSO
aconv, ALPHA_CONV, GEN_ALPHA_CONV.
\ENDDOC
|
