changeset 52037 | 837211662fb8 |
parent 47968 | 3119ad2b5ad3 |
child 54742 | 7a86358a3c0b |
--- a/src/HOL/TLA/Action.thy Thu May 16 15:21:12 2013 +0200 +++ b/src/HOL/TLA/Action.thy Thu May 16 17:39:38 2013 +0200 @@ -260,7 +260,7 @@ *) fun action_simp_tac ss intros elims = asm_full_simp_tac - (ss setloop ((resolve_tac ((map action_use intros) + (ss setloop (fn _ => (resolve_tac ((map action_use intros) @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI])) ORELSE' (eresolve_tac ((map action_use elims) @ [conjE,disjE,exE]))));