--- a/src/Doc/Tutorial/Protocol/Event.thy Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy Tue Feb 10 14:48:26 2015 +0100
@@ -262,7 +262,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
*}
@@ -333,7 +333,7 @@
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}])