--- a/src/HOL/TLA/TLA.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/TLA/TLA.thy Fri May 13 22:55:00 2011 +0200
@@ -583,11 +583,13 @@
ML {*
(* inv_tac reduces goals of the form ... ==> sigma |= []P *)
-fun inv_tac css = SELECT_GOAL
- (EVERY [auto_tac css,
- TRY (merge_box_tac 1),
- rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
- TRYALL (etac @{thm Stable})]);
+fun inv_tac ctxt =
+ SELECT_GOAL
+ (EVERY
+ [auto_tac ctxt,
+ TRY (merge_box_tac 1),
+ rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
+ TRYALL (etac @{thm Stable})]);
(* auto_inv_tac applies inv_tac and then tries to attack the subgoals
in simple cases it may be able to handle goals like |- MyProg --> []Inv.
@@ -595,15 +597,15 @@
auto-tactic, which applies too much propositional logic and simplifies
too late.
*)
-fun auto_inv_tac ss = SELECT_GOAL
- ((inv_tac (@{claset}, ss) 1) THEN
- (TRYALL (action_simp_tac
- (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
+fun auto_inv_tac ss =
+ SELECT_GOAL
+ (inv_tac (map_simpset_local (K ss) @{context}) 1 THEN
+ (TRYALL (action_simp_tac
+ (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
*}
method_setup invariant = {*
- Method.sections Clasimp.clasimp_modifiers
- >> (K (SIMPLE_METHOD' o inv_tac o clasimpset_of))
+ Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac))
*} ""
method_setup auto_invariant = {*