src/HOL/TLA/TLA.thy
changeset 51717 9e7d1c139569
parent 51668 5e1108291c7f
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/TLA/TLA.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -597,7 +597,7 @@
     1.4    SELECT_GOAL
     1.5      (inv_tac ctxt 1 THEN
     1.6        (TRYALL (action_simp_tac
     1.7 -        (simpset_of ctxt addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
     1.8 +        (ctxt addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
     1.9  *}
    1.10  
    1.11  method_setup invariant = {*