src/HOL/Auth/WooLam.thy
changeset 3519 ab0a9fbed4c0
parent 3481 256f38c01b98
child 3659 eddedfe2f3f8
--- a/src/HOL/Auth/WooLam.thy	Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy	Mon Jul 14 12:47:21 1997 +0200
@@ -16,8 +16,7 @@
 
 WooLam = Shared + 
 
-consts  lost    :: agent set        (*No need for it to be a variable*)
-	woolam  :: event list set
+consts  woolam  :: event list set
 inductive woolam
   intrs 
          (*Initial trace is empty*)
@@ -27,7 +26,7 @@
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
     Fake "[| evs: woolam;  B ~= Spy;  
-             X: synth (analz (sees lost Spy evs)) |]
+             X: synth (analz (sees Spy evs)) |]
           ==> Says Spy B X  # evs : woolam"
 
          (*Alice initiates a protocol run*)