author  lcp 
Wed, 27 Jul 1994 15:33:42 +0200  
changeset 488  52f7447d4f1b 
parent 484  70b789956bd3 
child 516  1957113f0d7d 
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 

488  31 
use_thy "InfDatatype"; 
124  32 
use_thy "ListFn"; 
0  33 

34 
(*printing functions are inherited from FOL*) 

35 
print_depth 8; 

36 

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