equal
deleted
inserted
replaced
6 Miscellaneous examples for Zermelo-Fraenkel Set Theory |
6 Miscellaneous examples for Zermelo-Fraenkel Set Theory |
7 Composition of homomorphisms, Pastre's examples, ... |
7 Composition of homomorphisms, Pastre's examples, ... |
8 *) |
8 *) |
9 |
9 |
10 writeln"ZF/ex/misc"; |
10 writeln"ZF/ex/misc"; |
|
11 |
|
12 (*Nice Blast_tac benchmark. Proved in 0.3s; old tactics can't manage it!*) |
|
13 goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"; |
|
14 by (Blast_tac 1); |
|
15 result(); |
11 |
16 |
12 set_current_thy"Perm"; |
17 set_current_thy"Perm"; |
13 |
18 |
14 (*Example 12 (credited to Peter Andrews) from |
19 (*Example 12 (credited to Peter Andrews) from |
15 W. Bledsoe. A Maximal Method for Set Variables in Automatic Theorem-proving. |
20 W. Bledsoe. A Maximal Method for Set Variables in Automatic Theorem-proving. |