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.
Uses ZF.thy again, to make that theory usable
authorpaulson
Wed, 02 Apr 1997 15:37:35 +0200
changeset 2876 02c12d4c8b97
parent 2875 6e3ccb94836c
child 2877 6476784dba1c
Uses ZF.thy again, to make that theory usable
src/ZF/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/simpdata.ML	Wed Apr 02 15:36:32 1997 +0200
+++ b/src/ZF/simpdata.ML	Wed Apr 02 15:37:35 1997 +0200
@@ -10,7 +10,7 @@
 
 (*For proving rewrite rules*)
 fun prove_fun s = 
-    (writeln s;  prove_goal thy s
+    (writeln s;  prove_goal ZF.thy s
        (fn prems => [ (cut_facts_tac prems 1), (Fast_tac 1) ]));
 
 (*Are all these really suitable?*)
isabelle