src/ZF/ROOT.ML
changeset 75 144ec40f2650
parent 50 37e93ef9c756
child 90 a90653dabebc
     1.1 --- a/src/ZF/ROOT.ML	Fri Oct 22 13:42:51 1993 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Fri Oct 22 13:43:45 1993 +0100
     1.3 @@ -11,6 +11,8 @@
     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 @@ -66,7 +68,7 @@
    1.13  use     "datatype.ML";
    1.14  
    1.15  use     "fin.ML";
    1.16 -use     "list.ML";
    1.17 +use_thy "List";
    1.18  use_thy "listfn";
    1.19  
    1.20  (*printing functions are inherited from FOL*)