src/ZF/ROOT.ML
changeset 124 858ab9a9b047
parent 120 09287f26bfb8
child 364 6573122322d7
     1.1 --- a/src/ZF/ROOT.ML	Tue Nov 16 14:23:19 1993 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Tue Nov 16 14:24:21 1993 +0100
     1.3 @@ -11,8 +11,6 @@
     1.4  val banner = "ZF Set Theory (in FOL)";
     1.5  writeln banner;
     1.6  
     1.7 -set_loadpath [".", "ex", "../FOL"];
     1.8 -
     1.9  (*For Pure/tactic??  A crude way of adding structure to rules*)
    1.10  fun CHECK_SOLVED (Tactic tf) = 
    1.11    Tactic (fn state => 
    1.12 @@ -29,47 +27,9 @@
    1.13  fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
    1.14  
    1.15  print_depth 1;
    1.16 -use_thy "zf";
    1.17  
    1.18 -use     "upair.ML";
    1.19 -use     "subset.ML";
    1.20 -use     "pair.ML";
    1.21 -use     "domrange.ML";
    1.22 -use     "func.ML";
    1.23 -use     "equalities.ML";
    1.24 -use     "simpdata.ML";  
    1.25 -
    1.26 -(*further development*)
    1.27 -use_thy "bool";
    1.28 -use_thy "sum";
    1.29 -use_thy "qpair";
    1.30 -use     "mono.ML";
    1.31 -use_thy "fixedpt";
    1.32 -
    1.33 -(*Inductive/coinductive definitions*)
    1.34 -use     "ind_syntax.ML";
    1.35 -use     "intr_elim.ML";
    1.36 -use     "indrule.ML";
    1.37 -use     "inductive.ML";
    1.38 -use     "coinductive.ML";
    1.39 -
    1.40 -use_thy "perm";
    1.41 -use_thy "trancl";
    1.42 -use_thy "wf";
    1.43 -use_thy "ord";
    1.44 -use_thy "nat";
    1.45 -use_thy "epsilon";
    1.46 -use_thy "arith";
    1.47 -
    1.48 -(*Datatype/codatatype definitions*)
    1.49 -use_thy "univ";
    1.50 -use_thy "quniv";
    1.51 -use     "constructor.ML";
    1.52 -use     "datatype.ML";
    1.53 -
    1.54 -use     "fin.ML";
    1.55 -use_thy "List";
    1.56 -use_thy "listfn";
    1.57 +use_thy "fin";
    1.58 +use_thy "ListFn";
    1.59  
    1.60  (*printing functions are inherited from FOL*)
    1.61  print_depth 8;