src/Doc/Tutorial/Protocol/Event.thy

 
 ML
 {*
 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
 *}
 
 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
 by (induct e, auto simp: knows_Cons)

 
 
 fun synth_analz_mono_contra_tac ctxt = 
   rtac @{thm syan_impI} THEN'
   REPEAT1 o 
-    (dresolve_tac 
+    (dresolve_tac ctxt
      [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
       @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
       @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
   THEN'
   mp_tac ctxt