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
35
36
|
\DOC GEN_ALL
\TYPE {GEN_ALL : thm -> thm}
\SYNOPSIS
Generalizes the conclusion of a theorem over its own free variables.
\KEYWORDS
rule, quantifier, universal.
\DESCRIBE
When applied to a theorem {A |- t}, the inference rule {GEN_ALL} returns
the theorem {A |- !x1...xn. t}, where the {xi} are all the variables,
if any, which are free in {t} but not in the assumptions.
{
A |- t
------------------ GEN_ALL
A |- !x1...xn. t
}
\FAILURE
Never fails.
\EXAMPLE
{
# let th = ARITH_RULE `x < y ==> 2 * x + y + 1 < 3 * y`;;
val th : thm = |- x < y ==> 2 * x + y + 1 < 3 * y
# GEN_ALL th;;
val it : thm = |- !x y. x < y ==> 2 * x + y + 1 < 3 * y
}
\SEEALSO
GEN, GENL, GEN_ALL, SPEC, SPECL, SPEC_ALL, SPEC_TAC.
\ENDDOC
|
