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.
'atomize': CHANGED_PROP;
authorwenzelm
Wed, 31 Oct 2001 22:00:25 +0100
changeset 12007 72f43e7c3315
parent 12006 72fd225a5aa2
child 12008 078637472921
'atomize': CHANGED_PROP;
src/Pure/Isar/method.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/method.ML	Wed Oct 31 22:00:02 2001 +0100
+++ b/src/Pure/Isar/method.ML	Wed Oct 31 22:00:25 2001 +0100
@@ -680,7 +680,7 @@
   ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
   ("unfold", thms_args unfold, "unfold definitions"),
   ("fold", thms_args fold, "fold definitions"),
-  ("atomize", no_args (SIMPLE_METHOD' HEADGOAL ObjectLogic.atomize_tac),
+  ("atomize", no_args (SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac)),
     "present local premises as object-level statements"),
   ("rule", thms_ctxt_args some_rule, "apply some rule"),
   ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
isabelle