changeset 60754 | 02924903a6fd |
parent 59498 | 50b60f501b05 |
child 63167 | 0909deb8059b |
--- a/src/HOL/SET_Protocol/Event_SET.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/SET_Protocol/Event_SET.thy Sat Jul 18 20:54:56 2015 +0200 @@ -183,7 +183,7 @@ ML {* fun analz_mono_contra_tac ctxt = - rtac @{thm analz_impI} THEN' + resolve_tac ctxt @{thms analz_impI} THEN' REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra}) THEN' mp_tac ctxt *}