src/HOL/Auth/Event.thy
changeset 21588 cd0dc678a205
parent 21404 eb85850d3eb7
child 24122 fc7f857d33c8
     1.1 --- a/src/HOL/Auth/Event.thy	Wed Nov 29 15:44:46 2006 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Wed Nov 29 15:44:51 2006 +0100
     1.3 @@ -290,8 +290,7 @@
     1.4      intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
     1.5  
     1.6  method_setup analz_mono_contra = {*
     1.7 -    Method.no_args
     1.8 -      (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
     1.9 +    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
    1.10      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
    1.11  
    1.12  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    1.13 @@ -349,8 +348,7 @@
    1.14  *}
    1.15  
    1.16  method_setup synth_analz_mono_contra = {*
    1.17 -    Method.no_args
    1.18 -      (Method.METHOD (fn facts => REPEAT_FIRST synth_analz_mono_contra_tac)) *}
    1.19 +    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
    1.20      "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
    1.21  
    1.22  end