src/HOL/Auth/Event.thy
changeset 11189 1ea763a5d186
parent 11104 f2024fed9f0c
child 11192 5fd02b905a9a
     1.1 --- a/src/HOL/Auth/Event.thy	Fri Mar 02 13:14:37 2001 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Fri Mar 02 13:18:31 2001 +0100
     1.3 @@ -14,12 +14,6 @@
     1.4  theory Event = Message
     1.5  files ("Event_lemmas.ML"):
     1.6  
     1.7 -(*from Message.ML*)
     1.8 -method_setup spy_analz = {*
     1.9 -    Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
    1.10 -    "for proving the Fake case when analz is involved"
    1.11 -
    1.12 -
    1.13  consts  (*Initial states of agents -- parameter of the construction*)
    1.14    initState :: "agent => msg set"
    1.15