src/HOL/TLA/TLA.thy
 changeset 42803 7ed59879b1b6 parent 42795 66fcc9882784 child 42814 5af15f1e2ef6
```     1.1 --- a/src/HOL/TLA/TLA.thy	Sat May 14 13:32:33 2011 +0200
1.2 +++ b/src/HOL/TLA/TLA.thy	Sat May 14 16:03:28 2011 +0200
1.3 @@ -597,11 +597,11 @@
1.4     auto-tactic, which applies too much propositional logic and simplifies
1.5     too late.
1.6  *)
1.7 -fun auto_inv_tac ss =
1.8 +fun auto_inv_tac ctxt =
1.9    SELECT_GOAL
1.10 -    (inv_tac (map_simpset (K ss) @{context}) 1 THEN
1.11 +    (inv_tac ctxt 1 THEN
1.12        (TRYALL (action_simp_tac
1.13 -        (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
1.14 +        (simpset_of ctxt addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
1.15  *}
1.16
1.17  method_setup invariant = {*
1.18 @@ -609,8 +609,7 @@
1.19  *} ""
1.20
1.21  method_setup auto_invariant = {*
1.22 -  Method.sections Clasimp.clasimp_modifiers
1.23 -    >> (K (SIMPLE_METHOD' o auto_inv_tac o simpset_of))
1.24 +  Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
1.25  *} ""
1.26
1.27  lemma unless: "|- [](\$P --> P` | Q`) --> (stable P) | <>Q"
```