equal
deleted
inserted
replaced
8 |
8 |
9 |
9 |
10 writeln"File HOL/ex/set."; |
10 writeln"File HOL/ex/set."; |
11 |
11 |
12 context Lfp.thy; |
12 context Lfp.thy; |
|
13 |
|
14 (*These two are cited in Benzmueller and Kohlhash's system description of LEO, |
|
15 CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*) |
|
16 |
|
17 Goal "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"; |
|
18 by (Blast_tac 1); |
|
19 result(); |
|
20 |
|
21 Goal "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"; |
|
22 by (Blast_tac 1); |
|
23 result(); |
13 |
24 |
14 (*trivial example of term synthesis: apparently hard for some provers!*) |
25 (*trivial example of term synthesis: apparently hard for some provers!*) |
15 Goal "a ~= b ==> a:?X & b ~: ?X"; |
26 Goal "a ~= b ==> a:?X & b ~: ?X"; |
16 by (Blast_tac 1); |
27 by (Blast_tac 1); |
17 result(); |
28 result(); |