--- a/src/HOL/Auth/Event.thy Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Auth/Event.thy Fri Mar 13 19:58:26 2009 +0100
@@ -289,7 +289,7 @@
*}
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 \<notin> analz (knows Spy evs) --> P"
subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
@@ -310,7 +310,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 \<notin> synth (analz (knows Spy evs)) --> P"
end