src/ZF/ROOT.ML
changeset 2469 b50b8c0eec01
parent 1512 ce37c64244c0
child 4262 e4113a682883
     1.1 --- a/src/ZF/ROOT.ML	Fri Jan 03 10:48:28 1997 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Fri Jan 03 15:01:55 1997 +0100
     1.3 @@ -11,6 +11,8 @@
     1.4  val banner = "ZF Set Theory (in FOL)";
     1.5  writeln banner;
     1.6  
     1.7 +eta_contract:=false;
     1.8 +
     1.9  (*For Pure/tactic??  A crude way of adding structure to rules*)
    1.10  fun CHECK_SOLVED tac st =
    1.11      case Sequence.pull (tac st) of
    1.12 @@ -32,6 +34,8 @@
    1.13  use     "thy_syntax.ML";
    1.14  
    1.15  use_thy "Let";
    1.16 +use_thy "func";
    1.17 +use     "typechk.ML";
    1.18  use_thy "InfDatatype";
    1.19  use_thy "List";
    1.20  use_thy "EquivClass";