equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Authors: Krzysztof Grabczewski and L C Paulson |
3 Authors: Krzysztof Grabczewski and L C Paulson |
4 |
4 |
5 Quantifiers and union operator for ordinals. |
5 Quantifiers and union operator for ordinals. |
6 *) |
6 *) |
|
7 |
|
8 val oall_def = thm "oall_def"; |
|
9 val oex_def = thm "oex_def"; |
|
10 val OUnion_def = thm "OUnion_def"; |
7 |
11 |
8 (*** universal quantifier for ordinals ***) |
12 (*** universal quantifier for ordinals ***) |
9 |
13 |
10 val prems = Goalw [oall_def] |
14 val prems = Goalw [oall_def] |
11 "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"; |
15 "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"; |