--- a/src/HOL/Tools/meson.ML Sun Jan 07 21:40:49 2001 +0100
+++ b/src/HOL/Tools/meson.ML Sun Jan 07 21:41:56 2001 +0100
@@ -383,7 +383,8 @@
local
fun meson_meth ctxt =
- Method.SIMPLE_METHOD' HEADGOAL (CHANGED o meson_claset_tac (Classical.get_local_claset ctxt));
+ Method.SIMPLE_METHOD' HEADGOAL
+ (CHANGED_PROP o meson_claset_tac (Classical.get_local_claset ctxt));
in
--- a/src/Provers/clasimp.ML Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Provers/clasimp.ML Sun Jan 07 21:41:56 2001 +0100
@@ -315,8 +315,8 @@
fun auto_args m =
Method.bang_sectioned_args' clasimp_modifiers (Scan.lift (Scan.option (Args.nat -- Args.nat))) m;
-fun auto_meth None = clasimp_meth (CHANGED o auto_tac)
- | auto_meth (Some (m, n)) = clasimp_meth (CHANGED o (fn css => mk_auto_tac css m n));
+fun auto_meth None = clasimp_meth (CHANGED_PROP o auto_tac)
+ | auto_meth (Some (m, n)) = clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n));
(* theory setup *)
@@ -330,6 +330,6 @@
("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"),
("force", clasimp_method' force_tac, "force"),
("auto", auto_args auto_meth, "auto"),
- ("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]];
+ ("clarsimp", clasimp_method' (CHANGED_PROP oo clarsimp_tac), "clarify simplified goal")]];
end;
--- a/src/Provers/classical.ML Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Provers/classical.ML Sun Jan 07 21:41:56 2001 +0100
@@ -1192,11 +1192,11 @@
("contradiction", Method.no_args contradiction, "proof by contradiction"),
("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"),
("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"),
- ("clarify", cla_method' (CHANGED oo clarify_tac), "repeatedly apply safe steps"),
+ ("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"),
("fast", cla_method' fast_tac, "classical prover (depth-first)"),
("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
("best", cla_method' best_tac, "classical prover (best-first)"),
- ("safe", cla_method safe_tac, "classical prover (apply safe rules)")];
+ ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];
--- a/src/Provers/hypsubst.ML Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Provers/hypsubst.ML Sun Jan 07 21:41:56 2001 +0100
@@ -257,7 +257,8 @@
(* proof methods *)
val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac);
-val hyp_subst_meth = Method.no_args (Method.SIMPLE_METHOD' HEADGOAL hyp_subst_tac);
+val hyp_subst_meth =
+ Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac));
(* attributes *)
--- a/src/Provers/simplifier.ML Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Provers/simplifier.ML Sun Jan 07 21:41:56 2001 +0100
@@ -542,10 +542,11 @@
fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
ALLGOALS (Method.insert_tac (prems @ facts)) THEN
- (CHANGED o ALLGOALS o tac) (get_local_simpset ctxt));
+ (CHANGED_PROP o ALLGOALS o tac) (get_local_simpset ctxt));
fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ facts) THEN' (CHANGED oo tac) (get_local_simpset ctxt)));
+ HEADGOAL (Method.insert_tac (prems @ facts) THEN'
+ (CHANGED_PROP oo tac) (get_local_simpset ctxt)));
(* setup_methods *)
--- a/src/Provers/splitter.ML Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Provers/splitter.ML Sun Jan 07 21:41:56 2001 +0100
@@ -427,7 +427,7 @@
val split_args = #2 oo Method.syntax Attrib.local_thms;
-fun split_meth ths = Method.SIMPLE_METHOD' HEADGOAL (gen_split_tac ths);
+fun split_meth ths = Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths);
--- a/src/Pure/Isar/method.ML Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Pure/Isar/method.ML Sun Jan 07 21:41:56 2001 +0100
@@ -267,8 +267,8 @@
(* unfold / fold definitions *)
-fun unfold thms = SIMPLE_METHOD (CHANGED (rewrite_goals_tac thms));
-fun fold thms = SIMPLE_METHOD (CHANGED (fold_goals_tac thms));
+fun unfold thms = SIMPLE_METHOD (CHANGED_PROP (rewrite_goals_tac thms));
+fun fold thms = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac thms));
(* atomize meta-connectives *)
--- a/src/Pure/tctical.ML Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Pure/tctical.ML Sun Jan 07 21:41:56 2001 +0100
@@ -19,6 +19,7 @@
val APPEND : tactic * tactic -> tactic
val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
val CHANGED : tactic -> tactic
+ val CHANGED_PROP : tactic -> tactic
val CHANGED_GOAL : (int -> tactic) -> int -> tactic
val COND : (thm -> bool) -> tactic -> tactic -> tactic
val DETERM : tactic -> tactic
@@ -299,6 +300,12 @@
let fun diff st' = not (eq_thm(st,st'))
in Seq.filter diff (tac st) end;
+fun CHANGED_PROP tac st =
+ let
+ val prop = #prop (Thm.rep_thm st);
+ fun diff st' = not (prop aconv #prop (Thm.rep_thm st'));
+ in Seq.filter diff (tac st) end;
+
(*** Tacticals based on subgoal numbering ***)