src/HOL/Auth/Event.thy
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 32404 da3ca3c6ec81
     1.1 --- a/src/HOL/Auth/Event.thy	Mon Mar 16 17:51:24 2009 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Mon Mar 16 18:24:30 2009 +0100
     1.3 @@ -289,7 +289,7 @@
     1.4  *}
     1.5  
     1.6  method_setup analz_mono_contra = {*
     1.7 -    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
     1.8 +    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
     1.9      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
    1.10  
    1.11  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    1.12 @@ -310,7 +310,7 @@
    1.13  *}
    1.14  
    1.15  method_setup synth_analz_mono_contra = {*
    1.16 -    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
    1.17 +    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *}
    1.18      "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
    1.19  
    1.20  end