--- a/src/Pure/Isar/method.ML Mon Jan 21 15:29:06 2002 +0100
+++ b/src/Pure/Isar/method.ML Mon Jan 21 16:15:16 2002 +0100
@@ -182,6 +182,12 @@
fun fold ths = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac ths));
+(* atomize rule statements *)
+
+fun atomize false = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac)
+ | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
+
+
(* unfold intro/elim rules *)
fun intro ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
@@ -640,7 +646,7 @@
("intro", thms_args intro, "repeatedly apply introduction rules"),
("elim", thms_args elim, "repeatedly apply elimination rules"),
("fold", thms_args fold, "fold definitions"),
- ("atomize", no_args (SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac)),
+ ("atomize", (atomize o #2) oo syntax (Args.mode "full"),
"present local premises as object-level statements"),
("rules", rules_args rules_meth, "apply many rules, including proof search"),
("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
--- a/src/Pure/Isar/object_logic.ML Mon Jan 21 15:29:06 2002 +0100
+++ b/src/Pure/Isar/object_logic.ML Mon Jan 21 16:15:16 2002 +0100
@@ -18,6 +18,7 @@
val declare_rulify: theory attribute
val atomize_term: Sign.sg -> term -> term
val atomize_tac: int -> tactic
+ val full_atomize_tac: int -> tactic
val atomize_goal: int -> thm -> thm
val rulify: thm -> thm
val rulify_no_asm: thm -> thm
@@ -135,6 +136,9 @@
(rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st
else all_tac st;
+fun full_atomize_tac i st =
+ rewrite_goal_tac (get_atomize (Thm.sign_of_thm st)) i st;
+
fun atomize_goal i st =
(case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st');