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"