src/HOL/Auth/WooLam.thy

--- a/src/HOL/Auth/WooLam.thy	Tue Feb 27 12:28:42 2001 +0100
+++ b/src/HOL/Auth/WooLam.thy	Tue Feb 27 16:13:23 2001 +0100
@@ -20,46 +20,46 @@
 inductive woolam
   intrs 
          (*Initial trace is empty*)
-    Nil  "[]: woolam"
+    Nil  "[] \\<in> woolam"
 
          (** These rules allow agents to send messages to themselves **)
 
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-    Fake "[| evs: woolam;  X: synth (analz (spies evs)) |]
-          ==> Says Spy B X  # evs : woolam"
+    Fake "[| evsf \\<in> woolam;  X \\<in> synth (analz (spies evsf)) |]
+          ==> Says Spy B X  # evsf \\<in> woolam"
 
          (*Alice initiates a protocol run*)
-    WL1  "[| evs1: woolam |]
-          ==> Says A B (Agent A) # evs1 : woolam"
+    WL1  "[| evs1 \\<in> woolam |]
+          ==> Says A B (Agent A) # evs1 \\<in> woolam"
 
          (*Bob responds to Alice's message with a challenge.*)
-    WL2  "[| evs2: woolam;  Says A' B (Agent A) : set evs2 |]
-          ==> Says B A (Nonce NB) # evs2 : woolam"
+    WL2  "[| evs2 \\<in> woolam;  Says A' B (Agent A) \\<in> set evs2 |]
+          ==> Says B A (Nonce NB) # evs2 \\<in> woolam"
 
          (*Alice responds to Bob's challenge by encrypting NB with her key.
            B is *not* properly determined -- Alice essentially broadcasts
            her reply.*)
-    WL3  "[| evs3: woolam;
-             Says A  B (Agent A)  : set evs3;
-             Says B' A (Nonce NB) : set evs3 |]
-          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 : woolam"
+    WL3  "[| evs3 \\<in> woolam;
+             Says A  B (Agent A)  \\<in> set evs3;
+             Says B' A (Nonce NB) \\<in> set evs3 |]
+          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \\<in> woolam"
 
          (*Bob forwards Alice's response to the Server.  NOTE: usually
            the messages are shown in chronological order, for clarity.
            But here, exchanging the two events would cause the lemma
            WL4_analz_spies to pick up the wrong assumption!*)
-    WL4  "[| evs4: woolam;  
-             Says A'  B X         : set evs4;
-             Says A'' B (Agent A) : set evs4 |]
-          ==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam"
+    WL4  "[| evs4 \\<in> woolam;  
+             Says A'  B X         \\<in> set evs4;
+             Says A'' B (Agent A) \\<in> set evs4 |]
+          ==> Says B Server {|Agent A, Agent B, X|} # evs4 \\<in> woolam"
 
          (*Server decrypts Alice's response for Bob.*)
-    WL5  "[| evs5: woolam;  
+    WL5  "[| evs5 \\<in> woolam;  
              Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
-               : set evs5 |]
+               \\<in> set evs5 |]
           ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
-                 # evs5 : woolam"
+                 # evs5 \\<in> woolam"
 
 end