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 ABS
\TYPE {ABS : term -> thm -> thm}
\SYNOPSIS
Abstracts both sides of an equation.
\KEYWORDS
rule, abstraction.
\DESCRIBE
{
A |- t1 = t2
------------------------ ABS `x` [Where x is not free in A]
A |- (\x.t1) = (\x.t2)
}
\FAILURE
If the theorem is not an equation, or if the variable {x} is free in the
assumptions {A}.
\EXAMPLE
{
# ABS `m:num` (REFL `m:num`);;
val it : thm = |- (\m. m) = (\m. m)
}
\COMMENTS
This is one of HOL Light's 10 primitive inference rules.
\SEEALSO
ETA_CONV.
\ENDDOC
|
