--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ROOT.ML Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,74 @@
+(* Title: ZF/ROOT
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
+
+This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
+*)
+
+val banner = "ZF Set Theory (in FOL)";
+writeln banner;
+
+(*For Pure/drule?? Multiple resolution infixes*)
+infix 0 MRS MRL;
+
+(*Resolve a list of rules against bottom_rl from right to left*)
+fun rls MRS bottom_rl =
+ let fun rs_aux i [] = bottom_rl
+ | rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
+ in rs_aux 1 rls end;
+
+fun rlss MRL bottom_rls =
+ let fun rs_aux i [] = bottom_rls
+ | rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
+ in rs_aux 1 rlss end;
+
+print_depth 1;
+use_thy "zf";
+
+use "upair.ML";
+use "subset.ML";
+use "pair.ML";
+use "domrange.ML";
+use "func.ML";
+use "equalities.ML";
+use "simpdata.ML";
+
+(*further development*)
+use_thy "bool";
+use_thy "sum";
+use_thy "qpair";
+use "mono.ML";
+use_thy "fixedpt";
+
+(*Inductive/co-inductive definitions*)
+use "ind-syntax.ML";
+use "intr-elim.ML";
+use "indrule.ML";
+use "inductive.ML";
+use "co-inductive.ML";
+
+use_thy "perm";
+use_thy "trancl";
+use_thy "wf";
+use_thy "ordinal";
+use_thy "nat";
+use_thy "epsilon";
+use_thy "arith";
+
+(*Datatype/co-datatype definitions*)
+use_thy "univ";
+use_thy "quniv";
+use "constructor.ML";
+use "datatype.ML";
+
+use "fin.ML";
+use "list.ML";
+use_thy "list-fn";
+
+(*printing functions are inherited from FOL*)
+print_depth 8;
+
+val ZF_build_completed = (); (*indicate successful build*)