0

1 
(* Title: ZF/ROOT


2 
ID: $Id$


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 
(*For Pure/drule?? Multiple resolution infixes*)


15 
infix 0 MRS MRL;


16 


17 
(*Resolve a list of rules against bottom_rl from right to left*)


18 
fun rls MRS bottom_rl =


19 
let fun rs_aux i [] = bottom_rl


20 
 rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)


21 
in rs_aux 1 rls end;


22 


23 
fun rlss MRL bottom_rls =


24 
let fun rs_aux i [] = bottom_rls


25 
 rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)


26 
in rs_aux 1 rlss end;


27 


28 
print_depth 1;


29 
use_thy "zf";


30 


31 
use "upair.ML";


32 
use "subset.ML";


33 
use "pair.ML";


34 
use "domrange.ML";


35 
use "func.ML";


36 
use "equalities.ML";


37 
use "simpdata.ML";


38 


39 
(*further development*)


40 
use_thy "bool";


41 
use_thy "sum";


42 
use_thy "qpair";


43 
use "mono.ML";


44 
use_thy "fixedpt";


45 


46 
(*Inductive/coinductive definitions*)


47 
use "indsyntax.ML";


48 
use "intrelim.ML";


49 
use "indrule.ML";


50 
use "inductive.ML";


51 
use "coinductive.ML";


52 


53 
use_thy "perm";


54 
use_thy "trancl";


55 
use_thy "wf";


56 
use_thy "ordinal";


57 
use_thy "nat";


58 
use_thy "epsilon";


59 
use_thy "arith";


60 


61 
(*Datatype/codatatype definitions*)


62 
use_thy "univ";


63 
use_thy "quniv";


64 
use "constructor.ML";


65 
use "datatype.ML";


66 


67 
use "fin.ML";


68 
use "list.ML";


69 
use_thy "listfn";


70 


71 
(*printing functions are inherited from FOL*)


72 
print_depth 8;


73 


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