diff -r 80ca4a065a48 -r 02924903a6fd src/Doc/Tutorial/Protocol/Event.thy
--- a/src/Doc/Tutorial/Protocol/Event.thy	Sat Jul 18 20:53:05 2015 +0200
+++ b/src/Doc/Tutorial/Protocol/Event.thy	Sat Jul 18 20:54:56 2015 +0200
@@ -261,7 +261,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
 *}
@@ -331,7 +331,7 @@
 
 
 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},