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