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 CADE15, 1998 (page 139143) 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(); 