author  lcp 
Thu, 25 Aug 1994 12:09:21 +0200  
changeset 578  efc648d29dd0 
parent 532  851df239ac8b 
child 803  4c8333ab3eae 
permissions  rwrr 
0  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$ 
0  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
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 

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

14 
(*For Pure/tactic?? A crude way of adding structure to rules*) 
5  15 
fun CHECK_SOLVED (Tactic tf) = 
16 
Tactic (fn state => 

17 
case Sequence.pull (tf state) of 

18 
None => error"DO_GOAL: tactic list failed" 

19 
 Some(x,_) => 

20 
if has_fewer_prems 1 x then 

21 
Sequence.cons(x, Sequence.null) 

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

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

24 
print_goals (!goals_limit) x; 

25 
raise ERROR)); 

26 

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

28 

0  29 
print_depth 1; 
30 

516  31 
(*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

32 
use "../Pure/section_utils.ML"; 
516  33 
use_thy "Datatype"; 
34 
structure ThySyn = ThySynFun 

35 
(val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 

36 
"and", "", "<=", "domains", "intrs", "monos", 

37 
"con_defs", "type_intrs", "type_elims"] 

38 
and user_sections = [("inductive", inductive_decl ""), 

39 
("coinductive", inductive_decl "Co"), 

40 
("datatype", datatype_decl ""), 

41 
("codatatype", datatype_decl "Co")]); 

42 
init_thy_reader (); 

43 

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

46 
use_thy "EquivClass"; 
0  47 

48 
(*printing functions are inherited from FOL*) 

49 
print_depth 8; 

50 

51 
val ZF_build_completed = (); (*indicate successful build*) 