tuned ML setup;
authorwenzelm
Thu May 31 18:16:59 2007 +0200 (2007-05-31)
changeset 23168fcdd4346fa6b
parent 23167 b9bbdf7eab3b
child 23169 37091da05d8e
tuned ML setup;
src/ZF/ROOT.ML
src/ZF/ZF.thy
     1.1 --- a/src/ZF/ROOT.ML	Thu May 31 18:16:58 2007 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Thu May 31 18:16:59 2007 +0200
     1.3 @@ -11,8 +11,6 @@
     1.4  val banner = "ZF Set Theory (in FOL)";
     1.5  writeln banner;
     1.6  
     1.7 -reset eta_contract;
     1.8 -
     1.9  use_thy "Main_ZFC";
    1.10  
    1.11  Goal "True";  (*leave subgoal package empty*)
     2.1 --- a/src/ZF/ZF.thy	Thu May 31 18:16:58 2007 +0200
     2.2 +++ b/src/ZF/ZF.thy	Thu May 31 18:16:59 2007 +0200
     2.3 @@ -8,6 +8,8 @@
     2.4  
     2.5  theory ZF imports FOL begin
     2.6  
     2.7 +ML {* reset eta_contract *}
     2.8 +
     2.9  global
    2.10  
    2.11  typedecl i