changeset 59499 | 14095f771781 |
parent 59498 | 50b60f501b05 |
child 59755 | f8d164ab0dc1 |
--- a/src/CCL/CCL.thy Tue Feb 10 14:48:26 2015 +0100 +++ b/src/CCL/CCL.thy Tue Feb 10 16:46:21 2015 +0100 @@ -204,7 +204,8 @@ fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})] val inj_lemmas = maps mk_inj_lemmas rews in - CHANGED (REPEAT (ares_tac [@{thm iffI}, @{thm allI}, @{thm conjI}] i ORELSE + CHANGED (REPEAT (assume_tac ctxt i ORELSE + resolve_tac ctxt @{thms iffI allI conjI} i ORELSE eresolve_tac ctxt inj_lemmas i ORELSE asm_simp_tac (ctxt addsimps rews) i)) end;