| changeset 59498 | 50b60f501b05 |
| parent 58963 | 26bf09b95dda |
| child 60754 | 02924903a6fd |
--- a/src/HOL/SET_Protocol/Event_SET.thy Tue Feb 10 14:29:36 2015 +0100 +++ b/src/HOL/SET_Protocol/Event_SET.thy Tue Feb 10 14:48:26 2015 +0100 @@ -184,7 +184,7 @@ {* fun analz_mono_contra_tac ctxt = rtac @{thm analz_impI} THEN' - REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) + REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra}) THEN' mp_tac ctxt *}