Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned ML setup;
authorwenzelm
Thu, 31 May 2007 18:16:59 +0200
changeset 23168 fcdd4346fa6b
parent 23167 b9bbdf7eab3b
child 23169 37091da05d8e
tuned ML setup;
src/ZF/ROOT.ML file | annotate | diff | comparison | revisions
src/ZF/ZF.thy file | annotate | diff | comparison | revisions 
--- a/src/ZF/ROOT.ML	Thu May 31 18:16:58 2007 +0200
+++ b/src/ZF/ROOT.ML	Thu May 31 18:16:59 2007 +0200
@@ -11,8 +11,6 @@
 val banner = "ZF Set Theory (in FOL)";
 writeln banner;
 
-reset eta_contract;
-
 use_thy "Main_ZFC";
 
 Goal "True";  (*leave subgoal package empty*)
--- a/src/ZF/ZF.thy	Thu May 31 18:16:58 2007 +0200
+++ b/src/ZF/ZF.thy	Thu May 31 18:16:59 2007 +0200
@@ -8,6 +8,8 @@
 
 theory ZF imports FOL begin
 
+ML {* reset eta_contract *}
+
 global
 
 typedecl i
isabelle