src/HOL/TLA/Action.thy
changeset 59498 50b60f501b05
parent 58889 5b7a9633cfa8
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/TLA/Action.thy	Tue Feb 10 14:29:36 2015 +0100
     1.2 +++ b/src/HOL/TLA/Action.thy	Tue Feb 10 14:48:26 2015 +0100
     1.3 @@ -263,9 +263,9 @@
     1.4  *)
     1.5  fun action_simp_tac ctxt intros elims =
     1.6      asm_full_simp_tac
     1.7 -         (ctxt setloop (fn _ => (resolve_tac ((map (action_use ctxt) intros)
     1.8 +         (ctxt setloop (fn _ => (resolve_tac ctxt ((map (action_use ctxt) intros)
     1.9                                      @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
    1.10 -                      ORELSE' (eresolve_tac ((map (action_use ctxt) elims)
    1.11 +                      ORELSE' (eresolve_tac ctxt ((map (action_use ctxt) elims)
    1.12                                               @ [conjE,disjE,exE]))));
    1.13  *}
    1.14