# HG changeset patch
# User paulson
# Date 984556255 -3600
# Node ID bb01189f0565f5bc3da0092dae7a241b0b69dc46
# Parent  881222d487778b407f846b0d1929a4f700c9c125
minor tuning

diff -r 881222d48777 -r bb01189f0565 src/HOL/Auth/KerberosIV.ML
--- a/src/HOL/Auth/KerberosIV.ML	Tue Mar 13 18:35:48 2001 +0100
+++ b/src/HOL/Auth/KerberosIV.ML	Wed Mar 14 08:50:55 2001 +0100
@@ -185,8 +185,8 @@
 qed_spec_mp "new_keys_not_used";
 Addsimps [new_keys_not_used];
 
-(*Earlier, \\<forall>protocol proofs declared this theorem.  
-  But Yahalom and Kerberos IV are the only ones that need it!*)
+(*Earlier, all protocol proofs declared this theorem.  
+  But few of them actually need it! (Another is Yahalom) *)
 bind_thm ("new_keys_not_analzd",
           [analz_subset_parts RS keysFor_mono,
            new_keys_not_used] MRS contra_subsetD);
@@ -492,7 +492,7 @@
 by (blast_tac (claset() addSEs spies_partsEs) 1);
 qed "Serv_fresh_not_KeyCryptKey";
 
-Goalw [KeyCryptKey_def]
+Goal
  "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}\
 \             \\<in> parts (spies evs);  evs \\<in> kerberos |] \
 \        ==> ~ KeyCryptKey K AuthKey evs";
@@ -501,24 +501,23 @@
 (*K4*)
 by (blast_tac (claset() addEs spies_partsEs) 3);
 (*K2: by freshness*)
+by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 2); 
 by (blast_tac (claset() addEs spies_partsEs) 2);
 by (Fake_parts_insert_tac 1);
 qed "AuthKey_not_KeyCryptKey";
 
 (*A secure serverkey cannot have been used to encrypt others*)
-Goalw [KeyCryptKey_def]
- "[| Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} \
-\             \\<in> parts (spies evs);                     \
-\           Key ServKey \\<notin> analz (spies evs);             \
-\           B \\<noteq> Tgs;  evs \\<in> kerberos |] \
-\        ==> ~ KeyCryptKey ServKey K evs";
+Goal
+ "[| Crypt (shrK B) {|Agent A, Agent B, Key SK, tt|} \\<in> parts (spies evs); \
+\    Key SK \\<notin> analz (spies evs);             \
+\    B \\<noteq> Tgs;  evs \\<in> kerberos |] \
+\ ==> ~ KeyCryptKey SK K evs";
 by (etac rev_mp 1);
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 (*K4 splits into distinct subcases*)
-by (Step_tac 1);
-by (ALLGOALS Asm_full_simp_tac);
+by Auto_tac;  
 (*ServKey can't have been enclosed in two certificates*)
 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
                        addSEs [MPair_parts]
@@ -526,7 +525,7 @@
 (*ServKey is fresh and so could not have been used, by new_keys_not_used*)
 by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj,
 				Crypt_imp_invKey_keysFor],
-	       simpset()) 2); 
+	       simpset() addsimps [KeyCryptKey_def]) 2); 
 (*Others by freshness*)
 by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
 qed "ServKey_not_KeyCryptKey";
@@ -610,11 +609,6 @@
     REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE, exE]
 		  ORELSE' hyp_subst_tac)];
 
-Goal "[| KK <= -(range shrK); Key K \\<in> analz (spies evs); evs \\<in> kerberos |]   \
-\     ==> Key K \\<in> analz (Key ` KK Un spies evs)";
-by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1);
-qed "analz_mono_KK";
-
 (*For the Oops2 case of the next theorem*)
 Goal "[| evs \\<in> kerberos;  \
 \        Says Tgs A (Crypt AuthKey \
diff -r 881222d48777 -r bb01189f0565 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Tue Mar 13 18:35:48 2001 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Wed Mar 14 08:50:55 2001 +0100
@@ -17,10 +17,10 @@
 
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "B ~= Server   \
+Goal "B \\<noteq> Server   \
 \     ==> \\<exists>NA K. \\<exists>evs \\<in> otway.          \
 \            Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
-\              : set evs";
+\              \\<in> set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (otway.Nil RS 
           otway.OR1 RS otway.Reception RS
@@ -29,14 +29,14 @@
 by possibility_tac;
 result();
 
-Goal "[| Gets B X : set evs; evs : otway |] ==> \\<exists>A. Says A B X : set evs";
+Goal "[| Gets B X \\<in> set evs; evs \\<in> otway |] ==> \\<exists>A. Says A B X \\<in> set evs";
 by (etac rev_mp 1);
 by (etac otway.induct 1);
 by Auto_tac;
 qed"Gets_imp_Says";
 
 (*Must be proved separately for each protocol*)
-Goal "[| Gets B X : set evs; evs : otway |]  ==> X : knows Spy evs";
+Goal "[| Gets B X \\<in> set evs; evs \\<in> otway |]  ==> X \\<in> knows Spy evs";
 by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
 qed"Gets_imp_knows_Spy";
 AddSDs [Gets_imp_knows_Spy RS parts.Inj];
@@ -46,18 +46,18 @@
 
 (** For reasoning about the encrypted portion of messages **)
 
-Goal "[| Gets B {|N, Agent A, Agent B, X|} : set evs;  evs : otway |]  \
-\     ==> X : analz (knows Spy evs)";
+Goal "[| Gets B {|N, Agent A, Agent B, X|} \\<in> set evs;  evs \\<in> otway |]  \
+\     ==> X \\<in> analz (knows Spy evs)";
 by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
 qed "OR2_analz_knows_Spy";
 
-Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} : set evs;  evs : otway |] \
-\     ==> X : analz (knows Spy evs)";
+Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} \\<in> set evs;  evs \\<in> otway |] \
+\     ==> X \\<in> analz (knows Spy evs)";
 by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
 qed "OR4_analz_knows_Spy";
 
-Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\     ==> K : parts (knows Spy evs)";
+Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} \\<in> set evs \
+\     ==> K \\<in> parts (knows Spy evs)";
 by (Blast_tac 1);
 qed "Oops_parts_knows_Spy";
 
@@ -79,13 +79,13 @@
     sends messages containing X! **)
 
 (*Spy never sees a good agent's shared key!*)
-Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
+Goal "evs \\<in> otway ==> (Key (shrK A) \\<in> parts (knows Spy evs)) = (A \\<in> bad)";
 by (parts_induct_tac 1);
 by (ALLGOALS Blast_tac);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
-Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
+Goal "evs \\<in> otway ==> (Key (shrK A) \\<in> analz (knows Spy evs)) = (A \\<in> bad)";
 by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
@@ -98,8 +98,8 @@
 
 (*Describes the form of K and NA when the Server sends this message.  Also
   for Oops case.*)
-Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
-\        evs : otway |]                                           \
+Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
+\        evs \\<in> otway |]                                           \
 \     ==> K \\<notin> range shrK & (\\<exists>i. NA = Nonce i) & (\\<exists>j. NB = Nonce j)";
 by (etac rev_mp 1);
 by (etac otway.induct 1);
@@ -119,8 +119,8 @@
 (****
  The following is to prove theorems of the form
 
-  Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
-  Key K : analz (knows Spy evs)
+  Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) ==>
+  Key K \\<in> analz (knows Spy evs)
 
  A more general formula must be proved inductively.
 ****)
@@ -129,9 +129,9 @@
 (** Session keys are not used to encrypt other session keys **)
 
 (*The equality makes the induction hypothesis easier to apply*)
-Goal "evs : otway ==> ALL K KK. KK <= - (range shrK) -->           \
-\                      (Key K : analz (Key`KK Un (knows Spy evs))) =  \
-\                      (K : KK | Key K : analz (knows Spy evs))";
+Goal "evs \\<in> otway ==> ALL K KK. KK <= - (range shrK) -->           \
+\                      (Key K \\<in> analz (Key`KK Un (knows Spy evs))) =  \
+\                      (K \\<in> KK | Key K \\<in> analz (knows Spy evs))";
 by (etac otway.induct 1);
 by analz_knows_Spy_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -142,18 +142,18 @@
 qed_spec_mp "analz_image_freshK";
 
 
-Goal "[| evs : otway;  KAB \\<notin> range shrK |]               \
-\     ==> Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
-\         (K = KAB | Key K : analz (knows Spy evs))";
+Goal "[| evs \\<in> otway;  KAB \\<notin> range shrK |]               \
+\     ==> Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) =  \
+\         (K = KAB | Key K \\<in> analz (knows Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
 
 (*** The Key K uniquely identifies the Server's  message. **)
 
-Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
-\        Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
-\        evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
+Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   \\<in> set evs; \ 
+\        Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \\<in> set evs; \
+\        evs \\<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
 by (etac rev_mp 1);
 by (etac rev_mp 1);
 by (etac otway.induct 1);
@@ -166,21 +166,21 @@
 (**** Authenticity properties relating to NA ****)
 
 (*Only OR1 can have caused such a part of a message to appear.*)
-Goal "[| A \\<notin> bad;  evs : otway |]                             \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
+Goal "[| A \\<notin> bad;  evs \\<in> otway |]                             \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\<in> parts (knows Spy evs) --> \
 \     Says A B {|NA, Agent A, Agent B,                      \
 \                Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
-\       : set evs";
+\       \\<in> set evs";
 by (parts_induct_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "Crypt_imp_OR1";
 
 Goal "[| Gets B {|NA, Agent A, Agent B,                      \
-\                 Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\        A \\<notin> bad; evs : otway |]                             \
+\                 Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \
+\        A \\<notin> bad; evs \\<in> otway |]                             \
 \      ==> Says A B {|NA, Agent A, Agent B,                      \
 \                     Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
-\            : set evs";
+\            \\<in> set evs";
 by (blast_tac (claset() addDs [Crypt_imp_OR1]) 1);
 qed"Crypt_imp_OR1_Gets";
 
@@ -189,7 +189,7 @@
 
 Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (knows Spy evs); \
 \        Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (knows Spy evs); \
-\        evs : otway;  A \\<notin> bad |]                                   \
+\        evs \\<in> otway;  A \\<notin> bad |]                                   \
 \     ==> B = C";
 by (etac rev_mp 1);
 by (etac rev_mp 1);
@@ -202,8 +202,8 @@
 (*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   over-simplified version of this protocol: see OtwayRees_Bad.*)
-Goal "[| A \\<notin> bad;  evs : otway |]                      \
-\     ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
+Goal "[| A \\<notin> bad;  evs \\<in> otway |]                      \
+\     ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\<in> parts (knows Spy evs) --> \
 \         Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
 \           \\<notin> parts (knows Spy evs)";
 by (parts_induct_tac 1);
@@ -214,14 +214,14 @@
 
 (*Crucial property: If the encrypted message appears, and A has used NA
   to start a run, then it originated with the Server!*)
-Goal "[| A \\<notin> bad;  evs : otway |]                                  \
+Goal "[| A \\<notin> bad;  evs \\<in> otway |]                                  \
 \     ==> Says A B {|NA, Agent A, Agent B,                          \
-\                    Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs --> \
-\         Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs)          \
+\                    Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs --> \
+\         Crypt (shrK A) {|NA, Key K|} \\<in> parts (knows Spy evs)          \
 \         --> (\\<exists>NB. Says Server B                                     \
 \                        {|NA,                                          \
 \                          Crypt (shrK A) {|NA, Key K|},                \
-\                          Crypt (shrK B) {|NB, Key K|}|} : set evs)";
+\                          Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs)";
 by (parts_induct_tac 1);
 by (Blast_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
@@ -238,14 +238,14 @@
   bad form of this protocol, even though we can prove
   Spy_not_see_encrypted_key*)
 Goal "[| Says A  B {|NA, Agent A, Agent B,                       \
-\                Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\        Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
-\    A \\<notin> bad;  evs : otway |]                              \
+\                Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \
+\        Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\<in> set evs; \
+\    A \\<notin> bad;  evs \\<in> otway |]                              \
 \ ==> \\<exists>NB. Says Server B                                  \
 \              {|NA,                                        \
 \                Crypt (shrK A) {|NA, Key K|},              \
 \                Crypt (shrK B) {|NB, Key K|}|}             \
-\                : set evs";
+\                \\<in> set evs";
 by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1);
 qed "A_trusts_OR4";
 
@@ -254,10 +254,10 @@
     Does not in itself guarantee security: an attack could violate 
     the premises, e.g. by having A=Spy **)
 
-Goal "[| A \\<notin> bad;  B \\<notin> bad;  evs : otway |]                  \
+Goal "[| A \\<notin> bad;  B \\<notin> bad;  evs \\<in> otway |]                  \
 \ ==> Says Server B                                            \
 \       {|NA, Crypt (shrK A) {|NA, Key K|},                    \
-\         Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
+\         Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs -->         \
 \     Notes Spy {|NA, NB, Key K|} \\<notin> set evs -->               \
 \     Key K \\<notin> analz (knows Spy evs)";
 by (etac otway.induct 1);
@@ -278,9 +278,9 @@
 
 Goal "[| Says Server B                                           \
 \         {|NA, Crypt (shrK A) {|NA, Key K|},                    \
-\               Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
+\               Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs;        \
 \        Notes Spy {|NA, NB, Key K|} \\<notin> set evs;                 \
-\        A \\<notin> bad;  B \\<notin> bad;  evs : otway |]                    \
+\        A \\<notin> bad;  B \\<notin> bad;  evs \\<in> otway |]                    \
 \     ==> Key K \\<notin> analz (knows Spy evs)";
 by (blast_tac (claset() addDs [Says_Server_message_form] addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
@@ -289,10 +289,10 @@
 (*A's guarantee.  The Oops premise quantifies over NB because A cannot know
   what it is.*)
 Goal "[| Says A  B {|NA, Agent A, Agent B,                       \
-\                    Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\        Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+\                    Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \
+\        Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\<in> set evs; \
 \        ALL NB. Notes Spy {|NA, NB, Key K|} \\<notin> set evs;         \
-\        A \\<notin> bad;  B \\<notin> bad;  evs : otway |]                    \
+\        A \\<notin> bad;  B \\<notin> bad;  evs \\<in> otway |]                    \
 \     ==> Key K \\<notin> analz (knows Spy evs)";
 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
 qed "A_gets_good_key";
@@ -303,12 +303,12 @@
 (*Only OR2 can have caused such a part of a message to appear.  We do not
   know anything about X: it does NOT have to have the right form.*)
 Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
-\          : parts (knows Spy evs);  \
-\        B \\<notin> bad;  evs : otway |]                         \
+\          \\<in> parts (knows Spy evs);  \
+\        B \\<notin> bad;  evs \\<in> otway |]                         \
 \     ==> \\<exists>X. Says B Server                              \
 \                {|NA, Agent A, Agent B, X,                       \
 \                  Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
-\                : set evs";
+\                \\<in> set evs";
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
 by (ALLGOALS Blast_tac);
@@ -317,9 +317,9 @@
 
 (** The Nonce NB uniquely identifies B's  message. **)
 
-Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs); \
-\        Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(knows Spy evs); \
-\          evs : otway;  B \\<notin> bad |]             \
+Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \\<in> parts(knows Spy evs); \
+\        Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \\<in> parts(knows Spy evs); \
+\          evs \\<in> otway;  B \\<notin> bad |]             \
 \        ==> NC = NA & C = A";
 by (etac rev_mp 1);
 by (etac rev_mp 1);
@@ -330,16 +330,16 @@
 
 (*If the encrypted message appears, and B has used Nonce NB,
   then it originated with the Server!  Quite messy proof.*)
-Goal "[| B \\<notin> bad;  evs : otway |]                                    \
-\ ==> Crypt (shrK B) {|NB, Key K|} : parts (knows Spy evs)            \
+Goal "[| B \\<notin> bad;  evs \\<in> otway |]                                    \
+\ ==> Crypt (shrK B) {|NB, Key K|} \\<in> parts (knows Spy evs)            \
 \     --> (ALL X'. Says B Server                                      \
 \                    {|NA, Agent A, Agent B, X',                      \
 \                      Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
-\          : set evs                                                  \
+\          \\<in> set evs                                                  \
 \          --> Says Server B                                          \
 \               {|NA, Crypt (shrK A) {|NA, Key K|},                   \
 \                     Crypt (shrK B) {|NB, Key K|}|}                  \
-\                   : set evs)";
+\                   \\<in> set evs)";
 by (asm_full_simp_tac (simpset() addsimps []) 1); 
 by (parts_induct_tac 1);
 by (Blast_tac 1);
@@ -357,14 +357,14 @@
   has sent the correct message.*)
 Goal "[| Says B Server {|NA, Agent A, Agent B, X',              \
 \                        Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
-\          : set evs;                                           \
-\        Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
-\        B \\<notin> bad;  evs : otway |]                              \
+\          \\<in> set evs;                                           \
+\        Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs;   \
+\        B \\<notin> bad;  evs \\<in> otway |]                              \
 \     ==> Says Server B                                         \
 \              {|NA,                                            \
 \                Crypt (shrK A) {|NA, Key K|},                  \
 \                Crypt (shrK B) {|NB, Key K|}|}                 \
-\                : set evs";
+\                \\<in> set evs";
 by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
 qed "B_trusts_OR3";
 
@@ -372,10 +372,10 @@
 (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
 Goal "[| Says B Server {|NA, Agent A, Agent B, X',              \
 \                        Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
-\          : set evs;                                           \
-\        Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
+\          \\<in> set evs;                                           \
+\        Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs;   \
 \        Notes Spy {|NA, NB, Key K|} \\<notin> set evs;                \
-\        A \\<notin> bad;  B \\<notin> bad;  evs : otway |]                   \
+\        A \\<notin> bad;  B \\<notin> bad;  evs \\<in> otway |]                   \
 \     ==> Key K \\<notin> analz (knows Spy evs)";
 by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
 qed "B_gets_good_key";
@@ -383,11 +383,11 @@
 
 Goal "[| Says Server B                                       \
 \           {|NA, Crypt (shrK A) {|NA, Key K|},              \
-\             Crypt (shrK B) {|NB, Key K|}|} : set evs;      \
-\        B \\<notin> bad;  evs : otway |]                           \
+\             Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs;      \
+\        B \\<notin> bad;  evs \\<in> otway |]                           \
 \ ==> \\<exists>X. Says B Server {|NA, Agent A, Agent B, X,         \
 \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
-\             : set evs";
+\             \\<in> set evs";
 by (etac rev_mp 1);
 by (etac otway.induct 1);
 by (ALLGOALS Asm_simp_tac);
@@ -399,13 +399,13 @@
 (*After getting and checking OR4, agent A can trust that B has been active.
   We could probably prove that X has the expected form, but that is not
   strictly necessary for authentication.*)
-Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;        \
+Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\<in> set evs;        \
 \        Says A  B {|NA, Agent A, Agent B,                                \
-\                    Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\        A \\<notin> bad;  B \\<notin> bad;  evs : otway |]                             \
+\                    Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \
+\        A \\<notin> bad;  B \\<notin> bad;  evs \\<in> otway |]                             \
 \ ==> \\<exists>NB X. Says B Server {|NA, Agent A, Agent B, X,               \
 \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
-\                : set evs";
+\                \\<in> set evs";
 by (blast_tac (claset() delrules [Gets_imp_knows_Spy RS parts.Inj]
 			addSDs [A_trusts_OR4, OR3_imp_OR2]) 1);
 qed "A_auths_B";
diff -r 881222d48777 -r bb01189f0565 src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Mar 13 18:35:48 2001 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Wed Mar 14 08:50:55 2001 +0100
@@ -17,7 +17,7 @@
 
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "B ~= Server   \
+Goal "B \\<noteq> Server   \
 \     ==> \\<exists>K. \\<exists>NA. \\<exists>evs \\<in> otway.                                      \
 \          Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
 \            \\<in> set evs";
@@ -112,8 +112,8 @@
 (****
  The following is to prove theorems of the form
 
-  Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
-  Key K : analz (knows Spy evs)
+  Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) ==>
+  Key K \\<in> analz (knows Spy evs)
 
  A more general formula must be proved inductively.
 ****)
@@ -168,7 +168,7 @@
 (**** Authenticity properties relating to NA ****)
 
 (*If the encrypted message appears then it originated with the Server!*)
-Goal "[| A \\<notin> bad;  A ~= B;  evs \\<in> otway |]                 \
+Goal "[| A \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                 \
 \     ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \\<in> parts (knows Spy evs) \
 \      --> (\\<exists>NB. Says Server B                                          \
 \                   {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
@@ -186,7 +186,7 @@
   Freshness may be inferred from nonce NA.*)
 Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
 \         \\<in> set evs;                                                 \
-\        A \\<notin> bad;  A ~= B;  evs \\<in> otway |]                          \
+\        A \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                          \
 \     ==> \\<exists>NB. Says Server B                                       \
 \                 {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
 \                   Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
@@ -239,7 +239,7 @@
 Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
 \         \\<in> set evs;                                                 \
 \        ALL NB. Notes Spy {|NA, NB, Key K|} \\<notin> set evs;             \
-\        A \\<notin> bad;  B \\<notin> bad;  A ~= B;  evs \\<in> otway |]               \
+\        A \\<notin> bad;  B \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]               \
 \     ==> Key K \\<notin> analz (knows Spy evs)";
 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
 qed "A_gets_good_key";
@@ -248,7 +248,7 @@
 (**** Authenticity properties relating to NB ****)
 
 (*If the encrypted message appears then it originated with the Server!*)
-Goal "[| B \\<notin> bad;  A ~= B;  evs \\<in> otway |]                              \
+Goal "[| B \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                              \
 \ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \\<in> parts (knows Spy evs) \
 \     --> (\\<exists>NA. Says Server B                                          \
 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
@@ -266,7 +266,7 @@
   has sent the correct message in round 3.*)
 Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \          \\<in> set evs;                                                    \
-\        B \\<notin> bad;  A ~= B;  evs \\<in> otway |]                              \
+\        B \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                              \
 \     ==> \\<exists>NA. Says Server B                                           \
 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
@@ -279,7 +279,7 @@
 Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \         \\<in> set evs;                                                     \
 \        ALL NA. Notes Spy {|NA, NB, Key K|} \\<notin> set evs;                 \
-\        A \\<notin> bad;  B \\<notin> bad;  A ~= B;  evs \\<in> otway |]                   \
+\        A \\<notin> bad;  B \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                   \
 \     ==> Key K \\<notin> analz (knows Spy evs)";
 by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
 qed "B_gets_good_key";
diff -r 881222d48777 -r bb01189f0565 src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Mar 13 18:35:48 2001 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Wed Mar 14 08:50:55 2001 +0100
@@ -19,7 +19,7 @@
 AddDs  [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "B ~= Server   \
+Goal "B \\<noteq> Server   \
 \     ==> \\<exists>K. \\<exists>NA. \\<exists>evs \\<in> otway.          \
 \           Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
 \             \\<in> set evs";
@@ -207,9 +207,9 @@
 (*** Attempting to prove stronger properties ***)
 
 (*Only OR1 can have caused such a part of a message to appear.
-  The premise A ~= B prevents OR2's similar-looking cryptogram from being
+  The premise A \\<noteq> B prevents OR2's similar-looking cryptogram from being
   picked up.  Original Otway-Rees doesn't need it.*)
-Goal "[| A \\<notin> bad;  A ~= B;  evs \\<in> otway |]                \
+Goal "[| A \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                \
 \     ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\<in> parts (knows Spy evs) --> \
 \         Says A B {|NA, Agent A, Agent B,                  \
 \                    Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \\<in> set evs";
@@ -220,10 +220,10 @@
 
 (*Crucial property: If the encrypted message appears, and A has used NA
   to start a run, then it originated with the Server!
-  The premise A ~= B allows use of Crypt_imp_OR1*)
+  The premise A \\<noteq> B allows use of Crypt_imp_OR1*)
 (*Only it is FALSE.  Somebody could make a fake message to Server
           substituting some other nonce NA' for NB.*)
-Goal "[| A \\<notin> bad;  A ~= B;  evs \\<in> otway |]                                \
+Goal "[| A \\<notin> bad;  A \\<noteq> B;  evs \\<in> otway |]                                \
 \     ==> Crypt (shrK A) {|NA, Key K|} \\<in> parts (knows Spy evs) -->    \
 \         Says A B {|NA, Agent A, Agent B,                        \
 \                    Crypt (shrK A) {|NA, Agent A, Agent B|}|}    \
diff -r 881222d48777 -r bb01189f0565 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Tue Mar 13 18:35:48 2001 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Wed Mar 14 08:50:55 2001 +0100
@@ -107,8 +107,8 @@
 qed_spec_mp "new_keys_not_used";
 Addsimps [new_keys_not_used];
 
-(*Earlier, \\<forall>protocol proofs declared this theorem.  
-  But Yahalom and Kerberos IV are the only ones that need it!*)
+(*Earlier, all protocol proofs declared this theorem.  
+  But few of them actually need it! (Another is Kerberos IV) *)
 bind_thm ("new_keys_not_analzd",
           [analz_subset_parts RS keysFor_mono,
            new_keys_not_used] MRS contra_subsetD);