--- a/src/HOL/Auth/Event.thy Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/Auth/Event.thy Sat Jul 18 20:54:56 2015 +0200
@@ -271,7 +271,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)
*}
@@ -287,7 +287,7 @@
ML
{*
fun synth_analz_mono_contra_tac ctxt =
- rtac @{thm syan_impI} THEN'
+ resolve_tac ctxt @{thms syan_impI} THEN'
REPEAT1 o
(dresolve_tac ctxt
[@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},