diff -r e19d5b459a61 -r 4120fc59dd85 doc-src/TutorialI/Protocol/Event.thy --- a/doc-src/TutorialI/Protocol/Event.thy Fri Mar 13 19:53:09 2009 +0100 +++ b/doc-src/TutorialI/Protocol/Event.thy Fri Mar 13 19:58:26 2009 +0100 @@ -287,7 +287,7 @@ intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD]) method_setup analz_mono_contra = {* - Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} + Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} "for proving theorems of the form X \ analz (knows Spy evs) --> P" subsubsection{*Useful for case analysis on whether a hash is a spoof or not*} @@ -344,7 +344,7 @@ *} method_setup synth_analz_mono_contra = {* - Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *} + Method.no_args (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *} "for proving theorems of the form X \ synth (analz (knows Spy evs)) --> P" (*>*)