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.
ObjectLogic.rulify;
authorwenzelm
Mon, 15 Oct 2001 20:35:42 +0200
changeset 11782 bdd2ac7c75ff
parent 11781 a08b62908caa
child 11783 aee100a086b1
ObjectLogic.rulify;
src/HOL/UNITY/Simple/NSP_Bad.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/UNITY/Simple/NSP_Bad.ML	Mon Oct 15 20:35:10 2001 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.ML	Mon Oct 15 20:35:42 2001 +0200
@@ -12,7 +12,7 @@
 *)
 
 fun impOfAlways th =
-  rulify (th RS Always_includes_reachable RS subsetD RS CollectD);
+  ObjectLogic.rulify (th RS Always_includes_reachable RS subsetD RS CollectD);
 
 AddEs spies_partsEs;
 AddDs [impOfSubs analz_subset_parts];
isabelle