author  paulson 
Fri, 03 Jan 1997 15:01:55 +0100  
changeset 2469  b50b8c0eec01 
parent 1512  ce37c64244c0 
child 4262  e4113a682883 
permissions  rwrr 
1461  1 
(* Title: ZF/ROOT 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
5
diff
changeset

2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

6 
Adds ZermeloFraenkel Set Theory to a database containing FirstOrder Logic. 

7 

8 
This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson. 

9 
*) 

10 

11 
val banner = "ZF Set Theory (in FOL)"; 

12 
writeln banner; 

13 

2469  14 
eta_contract:=false; 
15 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

16 
(*For Pure/tactic?? A crude way of adding structure to rules*) 
1512  17 
fun CHECK_SOLVED tac st = 
18 
case Sequence.pull (tac st) of 

1461  19 
None => error"DO_GOAL: tactic list failed" 
5  20 
 Some(x,_) => 
1461  21 
if has_fewer_prems 1 x then 
22 
Sequence.cons(x, Sequence.null) 

23 
else (writeln"DO_GOAL: unsolved goals!!"; 

24 
writeln"Final proof state was ..."; 

25 
print_goals (!goals_limit) x; 

1512  26 
raise ERROR); 
5  27 

28 
fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs)); 

29 

0  30 
print_depth 1; 
31 

516  32 
(*Add user sections for inductive/datatype definitions*) 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
532
diff
changeset

33 
use "../Pure/section_utils.ML"; 
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
578
diff
changeset

34 
use "thy_syntax.ML"; 
516  35 

1069
66efd8f90fbd
Now loads the theory "Let". Could add it to FOL, but this appears to
lcp
parents:
803
diff
changeset

36 
use_thy "Let"; 
2469  37 
use_thy "func"; 
38 
use "typechk.ML"; 

488  39 
use_thy "InfDatatype"; 
516  40 
use_thy "List"; 
532
851df239ac8b
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp
parents:
516
diff
changeset

41 
use_thy "EquivClass"; 
0  42 

43 
(*printing functions are inherited from FOL*) 

44 
print_depth 8; 

45 

1461  46 
val ZF_build_completed = (); (*indicate successful build*) 