set_of_list -> set
authornipkow
Thu Jun 26 13:20:50 1997 +0200 (1997-06-26)
changeset 3465e85c24717cad
parent 3464 315694e22856
child 3466 30791e5a69c4
set_of_list -> set
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Public.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Recur.thy
src/HOL/Auth/Shared.ML
src/HOL/Auth/WooLam.ML
src/HOL/Auth/WooLam.thy
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
src/HOL/List.ML
src/HOL/List.thy
src/HOL/ex/InSort.ML
src/HOL/ex/Qsort.ML
src/HOL/ex/Sorting.ML
src/HOL/ex/Sorting.thy
     1.1 --- a/src/HOL/Auth/NS_Public.ML	Thu Jun 26 11:58:05 1997 +0200
     1.2 +++ b/src/HOL/Auth/NS_Public.ML	Thu Jun 26 13:20:50 1997 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  (*A "possibility property": there are traces that reach the end*)
     1.5  goal thy 
     1.6   "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
     1.7 -\                     Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
     1.8 +\                     Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
     1.9  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.10  by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
    1.11  by possibility_tac;
    1.12 @@ -31,7 +31,7 @@
    1.13  (**** Inductive proofs about ns_public ****)
    1.14  
    1.15  (*Nobody sends themselves messages*)
    1.16 -goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set_of_list evs";
    1.17 +goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
    1.18  by (etac ns_public.induct 1);
    1.19  by (Auto_tac());
    1.20  qed_spec_mp "not_Says_to_self";
    1.21 @@ -134,7 +134,7 @@
    1.22  
    1.23  (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
    1.24  goal thy 
    1.25 - "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set_of_list evs; \
    1.26 + "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
    1.27  \           A ~: lost;  B ~: lost;  evs : ns_public |]                        \
    1.28  \        ==>  Nonce NA ~: analz (sees lost Spy evs)";
    1.29  by (etac rev_mp 1);
    1.30 @@ -157,12 +157,12 @@
    1.31  (*Authentication for A: if she receives message 2 and has used NA
    1.32    to start a run, then B has sent message 2.*)
    1.33  goal thy 
    1.34 - "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\
    1.35 + "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;\
    1.36  \           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
    1.37 -\             : set_of_list evs;\
    1.38 +\             : set evs;\
    1.39  \           A ~: lost;  B ~: lost;  evs : ns_public |]  \
    1.40  \        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
    1.41 -\              : set_of_list evs";
    1.42 +\              : set evs";
    1.43  by (etac rev_mp 1);
    1.44  (*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
    1.45  by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
    1.46 @@ -181,7 +181,7 @@
    1.47   "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
    1.48  \           Nonce NA ~: analz (sees lost Spy evs);                 \
    1.49  \           evs : ns_public |]                                     \
    1.50 -\   ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
    1.51 +\   ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
    1.52  by (etac rev_mp 1);
    1.53  by (etac rev_mp 1);
    1.54  by (analz_induct_tac 1);
    1.55 @@ -237,7 +237,7 @@
    1.56  (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
    1.57  goal thy 
    1.58   "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
    1.59 -\             : set_of_list evs;                                      \
    1.60 +\             : set evs;                                      \
    1.61  \           A ~: lost;  B ~: lost;  evs : ns_public |]                \
    1.62  \ ==> Nonce NB ~: analz (sees lost Spy evs)";
    1.63  by (etac rev_mp 1);
    1.64 @@ -262,10 +262,10 @@
    1.65    in message 2, then A has sent message 3.*)
    1.66  goal thy 
    1.67   "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
    1.68 -\             : set_of_list evs;                                       \
    1.69 -\           Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs;    \
    1.70 +\             : set evs;                                       \
    1.71 +\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;    \
    1.72  \           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
    1.73 -\        ==> Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
    1.74 +\        ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
    1.75  by (etac rev_mp 1);
    1.76  (*prepare induction over Crypt (pubK B) NB : parts H*)
    1.77  by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
    1.78 @@ -294,10 +294,10 @@
    1.79    NA, then A initiated the run using NA.  SAME proof as B_trusts_NS3!*)
    1.80  goal thy 
    1.81   "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
    1.82 -\             : set_of_list evs;                                       \
    1.83 -\           Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs;    \
    1.84 +\             : set evs;                                       \
    1.85 +\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;    \
    1.86  \           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
    1.87 -\    ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
    1.88 +\    ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
    1.89  by (etac rev_mp 1);
    1.90  (*prepare induction over Crypt (pubK B) {|NB|} : parts H*)
    1.91  by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
     2.1 --- a/src/HOL/Auth/NS_Public.thy	Thu Jun 26 11:58:05 1997 +0200
     2.2 +++ b/src/HOL/Auth/NS_Public.thy	Thu Jun 26 13:20:50 1997 +0200
     2.3 @@ -32,16 +32,15 @@
     2.4           (*Bob responds to Alice's message with a further nonce*)
     2.5      NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
     2.6               Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
     2.7 -               : set_of_list evs |]
     2.8 +               : set evs |]
     2.9            ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    2.10                  # evs  :  ns_public"
    2.11  
    2.12           (*Alice proves her existence by sending NB back to Bob.*)
    2.13      NS3  "[| evs: ns_public;  A ~= B;
    2.14 -             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
    2.15 -               : set_of_list evs;
    2.16 +             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
    2.17               Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    2.18 -               : set_of_list evs |]
    2.19 +               : set evs |]
    2.20            ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    2.21  
    2.22    (**Oops message??**)
     3.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Thu Jun 26 11:58:05 1997 +0200
     3.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Thu Jun 26 13:20:50 1997 +0200
     3.3 @@ -25,7 +25,7 @@
     3.4  (*A "possibility property": there are traces that reach the end*)
     3.5  goal thy 
     3.6   "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
     3.7 -\                     Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
     3.8 +\                     Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
     3.9  by (REPEAT (resolve_tac [exI,bexI] 1));
    3.10  by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
    3.11  by possibility_tac;
    3.12 @@ -35,7 +35,7 @@
    3.13  (**** Inductive proofs about ns_public ****)
    3.14  
    3.15  (*Nobody sends themselves messages*)
    3.16 -goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set_of_list evs";
    3.17 +goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
    3.18  by (etac ns_public.induct 1);
    3.19  by (Auto_tac());
    3.20  qed_spec_mp "not_Says_to_self";
    3.21 @@ -139,7 +139,7 @@
    3.22  
    3.23  (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
    3.24  goal thy 
    3.25 - "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set_of_list evs; \
    3.26 + "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
    3.27  \           A ~: lost;  B ~: lost;  evs : ns_public |]                        \
    3.28  \        ==>  Nonce NA ~: analz (sees lost Spy evs)";
    3.29  by (etac rev_mp 1);
    3.30 @@ -162,10 +162,10 @@
    3.31  (*Authentication for A: if she receives message 2 and has used NA
    3.32    to start a run, then B has sent message 2.*)
    3.33  goal thy 
    3.34 - "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\
    3.35 -\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set_of_list evs;\
    3.36 + "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;\
    3.37 +\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs;\
    3.38  \           A ~: lost;  B ~: lost;  evs : ns_public |]  \
    3.39 -\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set_of_list evs";
    3.40 +\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs";
    3.41  by (etac rev_mp 1);
    3.42  (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*)
    3.43  by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
    3.44 @@ -188,7 +188,7 @@
    3.45   "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
    3.46  \           Nonce NA ~: analz (sees lost Spy evs);                 \
    3.47  \           evs : ns_public |]                                     \
    3.48 -\   ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
    3.49 +\   ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
    3.50  by (etac rev_mp 1);
    3.51  by (etac rev_mp 1);
    3.52  by (analz_induct_tac 1);
    3.53 @@ -240,8 +240,8 @@
    3.54  
    3.55  (*NB remains secret PROVIDED Alice never responds with round 3*)
    3.56  goal thy 
    3.57 - "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs;\
    3.58 -\          (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set_of_list evs);  \
    3.59 + "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs;\
    3.60 +\          (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs);  \
    3.61  \          A ~: lost;  B ~: lost;  evs : ns_public |]   \
    3.62  \       ==> Nonce NB ~: analz (sees lost Spy evs)";
    3.63  by (etac rev_mp 1);
    3.64 @@ -270,10 +270,10 @@
    3.65    in message 2, then A has sent message 3--to somebody....*)
    3.66  goal thy 
    3.67   "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB|})          \
    3.68 -\             : set_of_list evs;                                       \
    3.69 -\           Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs;    \
    3.70 +\             : set evs;                                       \
    3.71 +\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;    \
    3.72  \           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
    3.73 -\        ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set_of_list evs";
    3.74 +\        ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs";
    3.75  by (etac rev_mp 1);
    3.76  (*prepare induction over Crypt (pubK B) NB : parts H*)
    3.77  by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
    3.78 @@ -295,7 +295,7 @@
    3.79  (*Can we strengthen the secrecy theorem?  NO*)
    3.80  goal thy 
    3.81   "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
    3.82 -\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs \
    3.83 +\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
    3.84  \     --> Nonce NB ~: analz (sees lost Spy evs)";
    3.85  by (analz_induct_tac 1);
    3.86  (*NS1*)
    3.87 @@ -321,14 +321,14 @@
    3.88  Level 9
    3.89  !!evs. [| A ~: lost; B ~: lost; evs : ns_public |]
    3.90         ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    3.91 -           : set_of_list evs -->
    3.92 +           : set evs -->
    3.93             Nonce NB ~: analz (sees lost Spy evs)
    3.94   1. !!evs Aa Ba B' NAa NBa evsa.
    3.95         [| A ~: lost; B ~: lost; evsa : ns_public; A ~= Ba;
    3.96 -          Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evsa;
    3.97 -          Says A Ba (Crypt (pubK Ba) {|Nonce NA, Agent A|}) : set_of_list evsa;
    3.98 +          Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa;
    3.99 +          Says A Ba (Crypt (pubK Ba) {|Nonce NA, Agent A|}) : set evsa;
   3.100            Ba : lost;
   3.101 -          Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evsa;
   3.102 +          Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa;
   3.103            Nonce NB ~: analz (sees lost Spy evsa) |]
   3.104         ==> False
   3.105  *)
     4.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Thu Jun 26 11:58:05 1997 +0200
     4.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Jun 26 13:20:50 1997 +0200
     4.3 @@ -35,17 +35,14 @@
     4.4  
     4.5           (*Bob responds to Alice's message with a further nonce*)
     4.6      NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
     4.7 -             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
     4.8 -               : set_of_list evs |]
     4.9 +             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
    4.10            ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    4.11                  # evs  :  ns_public"
    4.12  
    4.13           (*Alice proves her existence by sending NB back to Bob.*)
    4.14      NS3  "[| evs: ns_public;  A ~= B;
    4.15 -             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
    4.16 -               : set_of_list evs;
    4.17 -             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    4.18 -               : set_of_list evs |]
    4.19 +             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
    4.20 +             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs |]
    4.21            ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    4.22  
    4.23    (**Oops message??**)
     5.1 --- a/src/HOL/Auth/NS_Shared.ML	Thu Jun 26 11:58:05 1997 +0200
     5.2 +++ b/src/HOL/Auth/NS_Shared.ML	Thu Jun 26 13:20:50 1997 +0200
     5.3 @@ -23,7 +23,7 @@
     5.4  goal thy 
     5.5   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     5.6  \        ==> EX N K. EX evs: ns_shared lost.          \
     5.7 -\               Says A B (Crypt K {|Nonce N, Nonce N|}) : set_of_list evs";
     5.8 +\               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
     5.9  by (REPEAT (resolve_tac [exI,bexI] 1));
    5.10  by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
    5.11            ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
    5.12 @@ -44,7 +44,7 @@
    5.13  
    5.14  
    5.15  (*Nobody sends themselves messages*)
    5.16 -goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set_of_list evs";
    5.17 +goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set evs";
    5.18  by (etac ns_shared.induct 1);
    5.19  by (Auto_tac());
    5.20  qed_spec_mp "not_Says_to_self";
    5.21 @@ -52,13 +52,13 @@
    5.22  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    5.23  
    5.24  (*For reasoning about the encrypted portion of message NS3*)
    5.25 -goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set_of_list evs \
    5.26 +goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
    5.27  \                ==> X : parts (sees lost Spy evs)";
    5.28  by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    5.29  qed "NS3_msg_in_parts_sees_Spy";
    5.30                                
    5.31  goal thy
    5.32 -    "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set_of_list evs \
    5.33 +    "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
    5.34  \           ==> K : parts (sees lost Spy evs)";
    5.35  by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    5.36  qed "Oops_parts_sees_Spy";
    5.37 @@ -128,7 +128,7 @@
    5.38  (*Describes the form of K, X and K' when the Server sends this message.*)
    5.39  goal thy 
    5.40   "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
    5.41 -\             : set_of_list evs;                              \
    5.42 +\             : set evs;                              \
    5.43  \           evs : ns_shared lost |]                           \
    5.44  \        ==> K ~: range shrK &                                \
    5.45  \            X = (Crypt (shrK B) {|Key K, Agent A|}) &        \
    5.46 @@ -148,7 +148,7 @@
    5.47  \             Says Server A                                            \
    5.48  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
    5.49  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
    5.50 -\             : set_of_list evs";
    5.51 +\             : set evs";
    5.52  by (etac rev_mp 1);
    5.53  by parts_induct_tac;
    5.54  by (Fake_parts_insert_tac 1);
    5.55 @@ -161,7 +161,7 @@
    5.56    Use Says_Server_message_form if applicable.*)
    5.57  goal thy 
    5.58   "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
    5.59 -\            : set_of_list evs;  evs : ns_shared lost |]                   \
    5.60 +\            : set evs;  evs : ns_shared lost |]                   \
    5.61  \        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
    5.62  \            | X : analz (sees lost Spy evs)";
    5.63  by (case_tac "A : lost" 1);
    5.64 @@ -242,7 +242,7 @@
    5.65   "!!evs. evs : ns_shared lost ==>                                        \
    5.66  \      EX A' NA' B' X'. ALL A NA B X.                                    \
    5.67  \       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
    5.68 -\       : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'";
    5.69 +\       : set evs --> A=A' & NA=NA' & B=B' & X=X'";
    5.70  by (etac ns_shared.induct 1);
    5.71  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    5.72  by (Step_tac 1);
    5.73 @@ -260,10 +260,10 @@
    5.74  goal thy 
    5.75   "!!evs. [| Says Server A                                    \
    5.76  \             (Crypt (shrK A) {|NA, Agent B, Key K, X|})     \
    5.77 -\                  : set_of_list evs;                        \ 
    5.78 +\                  : set evs;                        \ 
    5.79  \           Says Server A'                                   \
    5.80  \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
    5.81 -\                  : set_of_list evs;                        \
    5.82 +\                  : set evs;                        \
    5.83  \           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
    5.84  by (prove_unique_tac lemma 1);
    5.85  qed "unique_session_keys";
    5.86 @@ -276,8 +276,8 @@
    5.87  \        ==> Says Server A                                             \
    5.88  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
    5.89  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
    5.90 -\             : set_of_list evs -->                                    \
    5.91 -\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \
    5.92 +\             : set evs -->                                    \
    5.93 +\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) --> \
    5.94  \        Key K ~: analz (sees lost Spy evs)";
    5.95  by (etac ns_shared.induct 1);
    5.96  by analz_sees_tac;
    5.97 @@ -308,8 +308,8 @@
    5.98  (*Final version: Server's message in the most abstract form*)
    5.99  goal thy 
   5.100   "!!evs. [| Says Server A                                               \
   5.101 -\            (Crypt K' {|NA, Agent B, Key K, X|}) : set_of_list evs;    \
   5.102 -\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs);  \
   5.103 +\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;    \
   5.104 +\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);  \
   5.105  \           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
   5.106  \        |] ==> Key K ~: analz (sees lost Spy evs)";
   5.107  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   5.108 @@ -320,8 +320,8 @@
   5.109  goal thy 
   5.110   "!!evs. [| C ~: {A,B,Server};                                          \
   5.111  \           Says Server A                                               \
   5.112 -\            (Crypt K' {|NA, Agent B, Key K, X|}) : set_of_list evs;    \
   5.113 -\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs);  \
   5.114 +\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;    \
   5.115 +\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);  \
   5.116  \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
   5.117  \        ==> Key K ~: analz (sees lost C evs)";
   5.118  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   5.119 @@ -344,7 +344,7 @@
   5.120  \         ==> EX NA. Says Server A                                     \
   5.121  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   5.122  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   5.123 -\             : set_of_list evs";
   5.124 +\             : set evs";
   5.125  by (etac rev_mp 1);
   5.126  by parts_induct_tac;
   5.127  by (Fake_parts_insert_tac 1);
   5.128 @@ -357,9 +357,9 @@
   5.129   "!!evs. [| B ~: lost;  evs : ns_shared lost |]            \
   5.130  \        ==> Key K ~: analz (sees lost Spy evs) -->             \
   5.131  \            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   5.132 -\            : set_of_list evs --> \
   5.133 +\            : set evs --> \
   5.134  \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->            \
   5.135 -\            Says B A (Crypt K (Nonce NB)) : set_of_list evs";
   5.136 +\            Says B A (Crypt K (Nonce NB)) : set evs";
   5.137  by (etac ns_shared.induct 1);
   5.138  by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   5.139  by (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5);
   5.140 @@ -390,10 +390,10 @@
   5.141  goal thy
   5.142   "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs);           \
   5.143  \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   5.144 -\           : set_of_list evs;                                        \
   5.145 -\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;  \
   5.146 +\           : set evs;                                        \
   5.147 +\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;  \
   5.148  \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
   5.149 -\        ==> Says B A (Crypt K (Nonce NB)) : set_of_list evs";
   5.150 +\        ==> Says B A (Crypt K (Nonce NB)) : set evs";
   5.151  by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
   5.152                         addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
   5.153  qed "A_trusts_NS4";
     6.1 --- a/src/HOL/Auth/NS_Shared.thy	Thu Jun 26 11:58:05 1997 +0200
     6.2 +++ b/src/HOL/Auth/NS_Shared.thy	Thu Jun 26 13:20:50 1997 +0200
     6.3 @@ -35,7 +35,7 @@
     6.4  	   Server doesn't know who the true sender is, hence the A' in
     6.5                 the sender field.*)
     6.6      NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
     6.7 -             Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
     6.8 +             Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs |]
     6.9            ==> Says Server A 
    6.10                  (Crypt (shrK A)
    6.11                     {|Nonce NA, Agent B, Key KAB,
    6.12 @@ -46,14 +46,14 @@
    6.13              Can inductively show A ~= Server*)
    6.14      NS3  "[| evs: ns_shared lost;  A ~= B;
    6.15               Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
    6.16 -               : set_of_list evs;
    6.17 -             Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    6.18 +               : set evs;
    6.19 +             Says A Server {|Agent A, Agent B, Nonce NA|} : set evs |]
    6.20            ==> Says A B X # evs : ns_shared lost"
    6.21  
    6.22           (*Bob's nonce exchange.  He does not know who the message came
    6.23             from, but responds to A because she is mentioned inside.*)
    6.24      NS4  "[| evs: ns_shared lost;  A ~= B;  Nonce NB ~: used evs;
    6.25 -             Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |]
    6.26 +             Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs |]
    6.27            ==> Says B A (Crypt K (Nonce NB)) # evs
    6.28                  : ns_shared lost"
    6.29  
    6.30 @@ -63,18 +63,18 @@
    6.31             Letting the Spy add or subtract 1 lets him send ALL nonces.
    6.32             Instead we distinguish the messages by sending the nonce twice.*)
    6.33      NS5  "[| evs: ns_shared lost;  A ~= B;  
    6.34 -             Says B' A (Crypt K (Nonce NB)) : set_of_list evs;
    6.35 +             Says B' A (Crypt K (Nonce NB)) : set evs;
    6.36               Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    6.37 -               : set_of_list evs |]
    6.38 +               : set evs |]
    6.39            ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared lost"
    6.40    
    6.41           (*This message models possible leaks of session keys.
    6.42             The two Nonces identify the protocol run: the rule insists upon
    6.43             the true senders in order to make them accurate.*)
    6.44      Oops "[| evs: ns_shared lost;  A ~= Spy;
    6.45 -             Says B A (Crypt K (Nonce NB)) : set_of_list evs;
    6.46 +             Says B A (Crypt K (Nonce NB)) : set evs;
    6.47               Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    6.48 -               : set_of_list evs |]
    6.49 +               : set evs |]
    6.50            ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
    6.51  
    6.52  end
     7.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Jun 26 11:58:05 1997 +0200
     7.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Jun 26 13:20:50 1997 +0200
     7.3 @@ -26,7 +26,7 @@
     7.4   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     7.5  \        ==> EX K. EX NA. EX evs: otway lost.          \
     7.6  \               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
     7.7 -\                 : set_of_list evs";
     7.8 +\                 : set evs";
     7.9  by (REPEAT (resolve_tac [exI,bexI] 1));
    7.10  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    7.11  by possibility_tac;
    7.12 @@ -45,7 +45,7 @@
    7.13  qed "otway_mono";
    7.14  
    7.15  (*Nobody sends themselves messages*)
    7.16 -goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
    7.17 +goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
    7.18  by (etac otway.induct 1);
    7.19  by (Auto_tac());
    7.20  qed_spec_mp "not_Says_to_self";
    7.21 @@ -55,17 +55,17 @@
    7.22  
    7.23  (** For reasoning about the encrypted portion of messages **)
    7.24  
    7.25 -goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs \
    7.26 +goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
    7.27  \                ==> X : analz (sees lost Spy evs)";
    7.28  by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    7.29  qed "OR2_analz_sees_Spy";
    7.30  
    7.31 -goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
    7.32 +goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    7.33  \                ==> X : analz (sees lost Spy evs)";
    7.34  by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    7.35  qed "OR4_analz_sees_Spy";
    7.36  
    7.37 -goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
    7.38 +goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    7.39  \                 ==> K : parts (sees lost Spy evs)";
    7.40  by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    7.41  qed "Oops_parts_sees_Spy";
    7.42 @@ -150,7 +150,7 @@
    7.43    for Oops case.*)
    7.44  goal thy 
    7.45   "!!evs. [| Says Server B                                                 \
    7.46 -\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;   \
    7.47 +\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
    7.48  \           evs : otway lost |]                                           \
    7.49  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    7.50  by (etac rev_mp 1);
    7.51 @@ -212,7 +212,7 @@
    7.52  goal thy 
    7.53   "!!evs. evs : otway lost ==>                                                 \
    7.54  \   EX B' NA' NB' X'. ALL B NA NB X.                                          \
    7.55 -\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
    7.56 +\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
    7.57  \     B=B' & NA=NA' & NB=NB' & X=X'";
    7.58  by (etac otway.induct 1);
    7.59  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    7.60 @@ -229,9 +229,9 @@
    7.61  
    7.62  goal thy 
    7.63   "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
    7.64 -\            : set_of_list evs;                                    \ 
    7.65 +\            : set evs;                                    \ 
    7.66  \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
    7.67 -\            : set_of_list evs;                                    \
    7.68 +\            : set evs;                                    \
    7.69  \           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
    7.70  by (prove_unique_tac lemma 1);
    7.71  qed "unique_session_keys";
    7.72 @@ -247,7 +247,7 @@
    7.73  \             : parts (sees lost Spy evs) -->                      \
    7.74  \            Says A B {|NA, Agent A, Agent B,                      \
    7.75  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    7.76 -\             : set_of_list evs";
    7.77 +\             : set evs";
    7.78  by parts_induct_tac;
    7.79  by (Fake_parts_insert_tac 1);
    7.80  qed_spec_mp "Crypt_imp_OR1";
    7.81 @@ -300,12 +300,12 @@
    7.82  \    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs)      \
    7.83  \        --> Says A B {|NA, Agent A, Agent B,                          \
    7.84  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
    7.85 -\             : set_of_list evs -->                                    \
    7.86 +\             : set evs -->                                    \
    7.87  \            (EX NB. Says Server B                                     \
    7.88  \                 {|NA,                                                \
    7.89  \                   Crypt (shrK A) {|NA, Key K|},                      \
    7.90  \                   Crypt (shrK B) {|NB, Key K|}|}                     \
    7.91 -\                   : set_of_list evs)";
    7.92 +\                   : set evs)";
    7.93  by parts_induct_tac;
    7.94  by (Fake_parts_insert_tac 1);
    7.95  (*OR1: it cannot be a new Nonce, contradiction.*)
    7.96 @@ -335,16 +335,16 @@
    7.97    Spy_not_see_encrypted_key*)
    7.98  goal thy 
    7.99   "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   7.100 -\            : set_of_list evs;                                    \
   7.101 +\            : set evs;                                    \
   7.102  \           Says A B {|NA, Agent A, Agent B,                       \
   7.103  \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   7.104 -\            : set_of_list evs;                                    \
   7.105 +\            : set evs;                                    \
   7.106  \           A ~: lost;  A ~= Spy;  evs : otway lost |]             \
   7.107  \        ==> EX NB. Says Server B                                  \
   7.108  \                     {|NA,                                        \
   7.109  \                       Crypt (shrK A) {|NA, Key K|},              \
   7.110  \                       Crypt (shrK B) {|NB, Key K|}|}             \
   7.111 -\                       : set_of_list evs";
   7.112 +\                       : set evs";
   7.113  by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   7.114                         addEs  sees_Spy_partsEs) 1);
   7.115  qed "A_trusts_OR4";
   7.116 @@ -358,8 +358,8 @@
   7.117   "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   7.118  \        ==> Says Server B                                                 \
   7.119  \              {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   7.120 -\                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs -->      \
   7.121 -\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   7.122 +\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->      \
   7.123 +\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
   7.124  \            Key K ~: analz (sees lost Spy evs)";
   7.125  by (etac otway.induct 1);
   7.126  by analz_sees_tac;
   7.127 @@ -382,8 +382,8 @@
   7.128  goal thy 
   7.129   "!!evs. [| Says Server B                                                \
   7.130  \            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   7.131 -\                  Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;     \
   7.132 -\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;             \
   7.133 +\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;     \
   7.134 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;             \
   7.135  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   7.136  \        ==> Key K ~: analz (sees lost Spy evs)";
   7.137  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   7.138 @@ -395,8 +395,8 @@
   7.139   "!!evs. [| C ~: {A,B,Server};                                           \
   7.140  \           Says Server B                                                \
   7.141  \            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   7.142 -\                  Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;     \
   7.143 -\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;             \
   7.144 +\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;     \
   7.145 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;             \
   7.146  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   7.147  \        ==> Key K ~: analz (sees lost C evs)";
   7.148  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   7.149 @@ -417,7 +417,7 @@
   7.150  \            (EX X. Says B Server                              \
   7.151  \             {|NA, Agent A, Agent B, X,                       \
   7.152  \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   7.153 -\             : set_of_list evs)";
   7.154 +\             : set evs)";
   7.155  by parts_induct_tac;
   7.156  by (Fake_parts_insert_tac 1);
   7.157  by (ALLGOALS Blast_tac);
   7.158 @@ -458,11 +458,11 @@
   7.159  \        --> (ALL X'. Says B Server                                      \
   7.160  \                       {|NA, Agent A, Agent B, X',                      \
   7.161  \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   7.162 -\             : set_of_list evs                                          \
   7.163 +\             : set evs                                          \
   7.164  \             --> Says Server B                                          \
   7.165  \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   7.166  \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   7.167 -\                   : set_of_list evs)";
   7.168 +\                   : set evs)";
   7.169  by parts_induct_tac;
   7.170  by (Fake_parts_insert_tac 1);
   7.171  (*OR1: it cannot be a new Nonce, contradiction.*)
   7.172 @@ -486,15 +486,15 @@
   7.173  goal thy 
   7.174   "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
   7.175  \           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
   7.176 -\            : set_of_list evs;                                    \
   7.177 +\            : set evs;                                    \
   7.178  \           Says B Server {|NA, Agent A, Agent B, X',              \
   7.179  \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   7.180 -\            : set_of_list evs |]                                  \
   7.181 +\            : set evs |]                                  \
   7.182  \        ==> Says Server B                                         \
   7.183  \                 {|NA,                                            \
   7.184  \                   Crypt (shrK A) {|NA, Key K|},                  \
   7.185  \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   7.186 -\                   : set_of_list evs";
   7.187 +\                   : set evs";
   7.188  by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   7.189                         addSEs sees_Spy_partsEs) 1);
   7.190  qed "B_trusts_OR3";
   7.191 @@ -507,10 +507,10 @@
   7.192   "!!evs. [| B ~: lost;  evs : otway lost |]                           \
   7.193  \        ==> Says Server B                                            \
   7.194  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   7.195 -\                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
   7.196 +\                Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
   7.197  \            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
   7.198  \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   7.199 -\            : set_of_list evs)";
   7.200 +\            : set evs)";
   7.201  by (etac otway.induct 1);
   7.202  by (ALLGOALS Asm_simp_tac);
   7.203  by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
   7.204 @@ -524,14 +524,14 @@
   7.205    strictly necessary for authentication.*)
   7.206  goal thy 
   7.207   "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   7.208 -\            : set_of_list evs;                                    \
   7.209 +\            : set evs;                                    \
   7.210  \           Says A B {|NA, Agent A, Agent B,                       \
   7.211  \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   7.212 -\            : set_of_list evs;                                    \
   7.213 +\            : set evs;                                    \
   7.214  \           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
   7.215  \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
   7.216  \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   7.217 -\            : set_of_list evs";
   7.218 +\            : set evs";
   7.219  by (blast_tac (!claset addSDs  [A_trusts_OR4]
   7.220                         addSEs [OR3_imp_OR2]) 1);
   7.221  qed "A_auths_B";
     8.1 --- a/src/HOL/Auth/OtwayRees.thy	Thu Jun 26 11:58:05 1997 +0200
     8.2 +++ b/src/HOL/Auth/OtwayRees.thy	Thu Jun 26 13:20:50 1997 +0200
     8.3 @@ -37,7 +37,7 @@
     8.4  	   the sender is, hence the A' in the sender field.
     8.5             Note that NB is encrypted.*)
     8.6      OR2  "[| evs: otway lost;  B ~= Server;  Nonce NB ~: used evs;
     8.7 -             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
     8.8 +             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
     8.9            ==> Says B Server 
    8.10                    {|Nonce NA, Agent A, Agent B, X, 
    8.11                      Crypt (shrK B)
    8.12 @@ -52,7 +52,7 @@
    8.13                    {|Nonce NA, Agent A, Agent B, 
    8.14                      Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
    8.15                      Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
    8.16 -               : set_of_list evs |]
    8.17 +               : set evs |]
    8.18            ==> Says Server B 
    8.19                    {|Nonce NA, 
    8.20                      Crypt (shrK A) {|Nonce NA, Key KAB|},
    8.21 @@ -65,16 +65,16 @@
    8.22               Says B Server {|Nonce NA, Agent A, Agent B, X', 
    8.23                               Crypt (shrK B)
    8.24                                     {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
    8.25 -               : set_of_list evs;
    8.26 +               : set evs;
    8.27               Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    8.28 -               : set_of_list evs |]
    8.29 +               : set evs |]
    8.30            ==> Says B A {|Nonce NA, X|} # evs : otway lost"
    8.31  
    8.32           (*This message models possible leaks of session keys.  The nonces
    8.33             identify the protocol run.*)
    8.34      Oops "[| evs: otway lost;  B ~= Spy;
    8.35               Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    8.36 -               : set_of_list evs |]
    8.37 +               : set evs |]
    8.38            ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
    8.39  
    8.40  end
     9.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jun 26 11:58:05 1997 +0200
     9.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Jun 26 13:20:50 1997 +0200
     9.3 @@ -23,7 +23,7 @@
     9.4   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                               \
     9.5  \        ==> EX K. EX NA. EX evs: otway lost.                                 \
     9.6  \             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
     9.7 -\             : set_of_list evs";
     9.8 +\             : set evs";
     9.9  by (REPEAT (resolve_tac [exI,bexI] 1));
    9.10  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    9.11  by possibility_tac;
    9.12 @@ -42,7 +42,7 @@
    9.13  qed "otway_mono";
    9.14  
    9.15  (*Nobody sends themselves messages*)
    9.16 -goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
    9.17 +goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
    9.18  by (etac otway.induct 1);
    9.19  by (Auto_tac());
    9.20  qed_spec_mp "not_Says_to_self";
    9.21 @@ -52,13 +52,13 @@
    9.22  
    9.23  (** For reasoning about the encrypted portion of messages **)
    9.24  
    9.25 -goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
    9.26 +goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
    9.27  \                X : analz (sees lost Spy evs)";
    9.28  by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    9.29  qed "OR4_analz_sees_Spy";
    9.30  
    9.31  goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    9.32 -\                  : set_of_list evs ==> K : parts (sees lost Spy evs)";
    9.33 +\                  : set evs ==> K : parts (sees lost Spy evs)";
    9.34  by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    9.35  qed "Oops_parts_sees_Spy";
    9.36  
    9.37 @@ -139,7 +139,7 @@
    9.38   "!!evs. [| Says Server B                                           \
    9.39  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    9.40  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    9.41 -\             : set_of_list evs;                                    \
    9.42 +\             : set evs;                                    \
    9.43  \           evs : otway lost |]                                     \
    9.44  \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    9.45  by (etac rev_mp 1);
    9.46 @@ -202,7 +202,7 @@
    9.47  \      EX A' B' NA' NB'. ALL A B NA NB.                    \
    9.48  \       Says Server B \
    9.49  \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
    9.50 -\           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs  \
    9.51 +\           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs  \
    9.52  \       --> A=A' & B=B' & NA=NA' & NB=NB'";
    9.53  by (etac otway.induct 1);
    9.54  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    9.55 @@ -222,11 +222,11 @@
    9.56  "!!evs. [| Says Server B                                           \
    9.57  \            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
    9.58  \              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
    9.59 -\           : set_of_list evs;                                     \
    9.60 +\           : set evs;                                     \
    9.61  \          Says Server B'                                          \
    9.62  \            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
    9.63  \              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
    9.64 -\           : set_of_list evs;                                     \
    9.65 +\           : set evs;                                     \
    9.66  \          evs : otway lost |]                                     \
    9.67  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
    9.68  by (prove_unique_tac lemma 1);
    9.69 @@ -244,7 +244,7 @@
    9.70  \     --> (EX NB. Says Server B                                          \
    9.71  \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
    9.72  \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
    9.73 -\                  : set_of_list evs)";
    9.74 +\                  : set evs)";
    9.75  by parts_induct_tac;
    9.76  by (Fake_parts_insert_tac 1);
    9.77  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
    9.78 @@ -257,12 +257,12 @@
    9.79    Freshness may be inferred from nonce NA.*)
    9.80  goal thy 
    9.81   "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
    9.82 -\            : set_of_list evs;                                         \
    9.83 +\            : set evs;                                         \
    9.84  \           A ~: lost;  evs : otway lost |]                             \
    9.85  \        ==> EX NB. Says Server B                                       \
    9.86  \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
    9.87  \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
    9.88 -\                   : set_of_list evs";
    9.89 +\                   : set evs";
    9.90  by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    9.91                        addEs  sees_Spy_partsEs) 1);
    9.92  qed "A_trusts_OR4";
    9.93 @@ -277,8 +277,8 @@
    9.94  \        ==> Says Server B                                                 \
    9.95  \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
    9.96  \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
    9.97 -\            : set_of_list evs -->                                         \
    9.98 -\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
    9.99 +\            : set evs -->                                         \
   9.100 +\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
   9.101  \            Key K ~: analz (sees lost Spy evs)";
   9.102  by (etac otway.induct 1);
   9.103  by analz_sees_tac;
   9.104 @@ -302,8 +302,8 @@
   9.105   "!!evs. [| Says Server B                                           \
   9.106  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   9.107  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   9.108 -\             : set_of_list evs;                                    \
   9.109 -\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;        \
   9.110 +\             : set evs;                                    \
   9.111 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;        \
   9.112  \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   9.113  \        ==> Key K ~: analz (sees lost Spy evs)";
   9.114  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   9.115 @@ -316,8 +316,8 @@
   9.116  \           Says Server B                                           \
   9.117  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   9.118  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   9.119 -\             : set_of_list evs;                                    \
   9.120 -\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;        \
   9.121 +\             : set evs;                                    \
   9.122 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;        \
   9.123  \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   9.124  \        ==> Key K ~: analz (sees lost C evs)";
   9.125  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   9.126 @@ -337,7 +337,7 @@
   9.127  \        --> (EX NA. Says Server B                                          \
   9.128  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   9.129  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   9.130 -\                     : set_of_list evs)";
   9.131 +\                     : set evs)";
   9.132  by parts_induct_tac;
   9.133  by (Fake_parts_insert_tac 1);
   9.134  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   9.135 @@ -351,11 +351,11 @@
   9.136  goal thy 
   9.137   "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   9.138  \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   9.139 -\            : set_of_list evs |]                                           \
   9.140 +\            : set evs |]                                           \
   9.141  \        ==> EX NA. Says Server B                                           \
   9.142  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   9.143  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   9.144 -\                     : set_of_list evs";
   9.145 +\                     : set evs";
   9.146  by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   9.147                         addEs  sees_Spy_partsEs) 1);
   9.148  qed "B_trusts_OR3";
    10.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Thu Jun 26 11:58:05 1997 +0200
    10.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Thu Jun 26 13:20:50 1997 +0200
    10.3 @@ -39,7 +39,7 @@
    10.4           (*Bob's response to Alice's message.  Bob doesn't know who 
    10.5  	   the sender is, hence the A' in the sender field.*)
    10.6      OR2  "[| evs: otway lost;  B ~= Server;
    10.7 -             Says A' B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    10.8 +             Says A' B {|Agent A, Agent B, Nonce NA|} : set evs |]
    10.9            ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
   10.10                   # evs : otway lost"
   10.11  
   10.12 @@ -47,7 +47,7 @@
   10.13             session key to Bob with a packet for forwarding to Alice.*)
   10.14      OR3  "[| evs: otway lost;  B ~= Server;  A ~= B;  Key KAB ~: used evs;
   10.15               Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
   10.16 -               : set_of_list evs |]
   10.17 +               : set evs |]
   10.18            ==> Says Server B 
   10.19                 {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
   10.20                   Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
   10.21 @@ -57,9 +57,9 @@
   10.22  	   those in the message he previously sent the Server.*)
   10.23      OR4  "[| evs: otway lost;  A ~= B;
   10.24               Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
   10.25 -               : set_of_list evs;
   10.26 +               : set evs;
   10.27               Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
   10.28 -               : set_of_list evs |]
   10.29 +               : set evs |]
   10.30            ==> Says B A X # evs : otway lost"
   10.31  
   10.32           (*This message models possible leaks of session keys.  The nonces
   10.33 @@ -68,7 +68,7 @@
   10.34               Says Server B 
   10.35                        {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, 
   10.36                          Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
   10.37 -               : set_of_list evs |]
   10.38 +               : set evs |]
   10.39            ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
   10.40  
   10.41  end
    11.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jun 26 11:58:05 1997 +0200
    11.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jun 26 13:20:50 1997 +0200
    11.3 @@ -29,7 +29,7 @@
    11.4   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    11.5  \        ==> EX K. EX NA. EX evs: otway.          \
    11.6  \               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    11.7 -\                 : set_of_list evs";
    11.8 +\                 : set evs";
    11.9  by (REPEAT (resolve_tac [exI,bexI] 1));
   11.10  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
   11.11  by possibility_tac;
   11.12 @@ -39,7 +39,7 @@
   11.13  (**** Inductive proofs about otway ****)
   11.14  
   11.15  (*Nobody sends themselves messages*)
   11.16 -goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs";
   11.17 +goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
   11.18  by (etac otway.induct 1);
   11.19  by (Auto_tac());
   11.20  qed_spec_mp "not_Says_to_self";
   11.21 @@ -49,17 +49,17 @@
   11.22  
   11.23  (** For reasoning about the encrypted portion of messages **)
   11.24  
   11.25 -goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
   11.26 +goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \
   11.27  \                X : analz (sees lost Spy evs)";
   11.28  by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
   11.29  qed "OR2_analz_sees_Spy";
   11.30  
   11.31 -goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
   11.32 +goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \
   11.33  \                X : analz (sees lost Spy evs)";
   11.34  by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
   11.35  qed "OR4_analz_sees_Spy";
   11.36  
   11.37 -goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
   11.38 +goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
   11.39  \                 ==> K : parts (sees lost Spy evs)";
   11.40  by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   11.41  qed "Oops_parts_sees_Spy";
   11.42 @@ -140,7 +140,7 @@
   11.43    for Oops case.*)
   11.44  goal thy 
   11.45   "!!evs. [| Says Server B                                                 \
   11.46 -\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;   \
   11.47 +\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
   11.48  \           evs : otway |]                                                \
   11.49  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   11.50  by (etac rev_mp 1);
   11.51 @@ -201,7 +201,7 @@
   11.52  goal thy 
   11.53   "!!evs. evs : otway ==>                                                      \
   11.54  \   EX B' NA' NB' X'. ALL B NA NB X.                                          \
   11.55 -\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
   11.56 +\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
   11.57  \     B=B' & NA=NA' & NB=NB' & X=X'";
   11.58  by (etac otway.induct 1);
   11.59  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   11.60 @@ -218,9 +218,9 @@
   11.61  
   11.62  goal thy 
   11.63   "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
   11.64 -\            : set_of_list evs;                                    \ 
   11.65 +\            : set evs;                                    \ 
   11.66  \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
   11.67 -\            : set_of_list evs;                                    \
   11.68 +\            : set evs;                                    \
   11.69  \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
   11.70  by (prove_unique_tac lemma 1);
   11.71  qed "unique_session_keys";
   11.72 @@ -231,8 +231,8 @@
   11.73   "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
   11.74  \        ==> Says Server B                                            \
   11.75  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   11.76 -\                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
   11.77 -\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->      \
   11.78 +\                Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
   11.79 +\            Says B Spy {|NA, NB, Key K|} ~: set evs -->      \
   11.80  \            Key K ~: analz (sees lost Spy evs)";
   11.81  by (etac otway.induct 1);
   11.82  by analz_sees_tac;
   11.83 @@ -255,8 +255,8 @@
   11.84  goal thy 
   11.85   "!!evs. [| Says Server B                                                \
   11.86  \            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   11.87 -\                  Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;     \
   11.88 -\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;             \
   11.89 +\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;     \
   11.90 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;             \
   11.91  \           A ~: lost;  B ~: lost;  evs : otway |]                \
   11.92  \        ==> Key K ~: analz (sees lost Spy evs)";
   11.93  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   11.94 @@ -276,7 +276,7 @@
   11.95  \             : parts (sees lost Spy evs) -->                  \
   11.96  \            Says A B {|NA, Agent A, Agent B,                  \
   11.97  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
   11.98 -\             : set_of_list evs";
   11.99 +\             : set evs";
  11.100  by parts_induct_tac;
  11.101  by (Fake_parts_insert_tac 1);
  11.102  by (Blast_tac 1);
  11.103 @@ -292,12 +292,12 @@
  11.104  \        ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) --> \
  11.105  \            Says A B {|NA, Agent A, Agent B,                  \
  11.106  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
  11.107 -\             : set_of_list evs -->                            \
  11.108 +\             : set evs -->                            \
  11.109  \            (EX B NB. Says Server B                           \
  11.110  \                 {|NA,                                        \
  11.111  \                   Crypt (shrK A) {|NA, Key K|},              \
  11.112  \                   Crypt (shrK B) {|NB, Key K|}|}             \
  11.113 -\                   : set_of_list evs)";
  11.114 +\                   : set evs)";
  11.115  by parts_induct_tac;
  11.116  by (Fake_parts_insert_tac 1);
  11.117  (*OR1: it cannot be a new Nonce, contradiction.*)
  11.118 @@ -317,11 +317,11 @@
  11.119             {|Nonce NAa, Agent Aa, Agent A,
  11.120               Crypt (shrK Aa) {|Nonce NAa, Agent Aa, Agent A|}, Nonce NA,
  11.121               Crypt (shrK A) {|Nonce NAa, Agent Aa, Agent A|}|}
  11.122 -          : set_of_list evsa;
  11.123 +          : set evsa;
  11.124            Says A B
  11.125             {|Nonce NA, Agent A, Agent B,
  11.126               Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}|}
  11.127 -          : set_of_list evsa 
  11.128 +          : set evsa 
  11.129  *)
  11.130  writeln "GIVE UP! on NA_Crypt_imp_Server_msg";
  11.131  
    12.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Thu Jun 26 11:58:05 1997 +0200
    12.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Thu Jun 26 13:20:50 1997 +0200
    12.3 @@ -36,7 +36,7 @@
    12.4  	   the sender is, hence the A' in the sender field.
    12.5             We modify the published protocol by NOT encrypting NB.*)
    12.6      OR2  "[| evs: otway;  B ~= Server;  Nonce NB ~: used evs;
    12.7 -             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    12.8 +             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
    12.9            ==> Says B Server 
   12.10                    {|Nonce NA, Agent A, Agent B, X, Nonce NB,
   12.11                      Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
   12.12 @@ -51,7 +51,7 @@
   12.13                      Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
   12.14                      Nonce NB, 
   12.15                      Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
   12.16 -               : set_of_list evs |]
   12.17 +               : set evs |]
   12.18            ==> Says Server B 
   12.19                    {|Nonce NA, 
   12.20                      Crypt (shrK A) {|Nonce NA, Key KAB|},
   12.21 @@ -62,16 +62,16 @@
   12.22  	   those in the message he previously sent the Server.*)
   12.23      OR4  "[| evs: otway;  A ~= B;
   12.24               Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
   12.25 -               : set_of_list evs;
   12.26 +               : set evs;
   12.27               Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
   12.28 -               : set_of_list evs |]
   12.29 +               : set evs |]
   12.30            ==> Says B A {|Nonce NA, X|} # evs : otway"
   12.31  
   12.32           (*This message models possible leaks of session keys.  The nonces
   12.33             identify the protocol run.*)
   12.34      Oops "[| evs: otway;  B ~= Spy;
   12.35               Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
   12.36 -               : set_of_list evs |]
   12.37 +               : set evs |]
   12.38            ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
   12.39  
   12.40  end
    13.1 --- a/src/HOL/Auth/Public.ML	Thu Jun 26 11:58:05 1997 +0200
    13.2 +++ b/src/HOL/Auth/Public.ML	Thu Jun 26 13:20:50 1997 +0200
    13.3 @@ -119,7 +119,7 @@
    13.4  				            setloop split_tac [expand_if]))));
    13.5  qed "UN_parts_sees_Says";
    13.6  
    13.7 -goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
    13.8 +goal thy "Says A B X : set evs --> X : sees lost Spy evs";
    13.9  by (list.induct_tac "evs" 1);
   13.10  by (Auto_tac ());
   13.11  qed_spec_mp "Says_imp_sees_Spy";
    14.1 --- a/src/HOL/Auth/Recur.ML	Thu Jun 26 11:58:05 1997 +0200
    14.2 +++ b/src/HOL/Auth/Recur.ML	Thu Jun 26 13:20:50 1997 +0200
    14.3 @@ -25,7 +25,7 @@
    14.4  \ ==> EX K NA. EX evs: recur lost.          \
    14.5  \     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
    14.6  \                     Agent Server|}      \
    14.7 -\         : set_of_list evs";
    14.8 +\         : set evs";
    14.9  by (REPEAT (resolve_tac [exI,bexI] 1));
   14.10  by (rtac (recur.Nil RS recur.RA1 RS 
   14.11            (respond.One RSN (4,recur.RA3))) 2);
   14.12 @@ -39,7 +39,7 @@
   14.13  \ ==> EX K. EX NA. EX evs: recur lost.            \
   14.14  \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
   14.15  \                  Agent Server|}                               \
   14.16 -\         : set_of_list evs";
   14.17 +\         : set evs";
   14.18  by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
   14.19  by (REPEAT (eresolve_tac [exE, conjE] 1));
   14.20  by (REPEAT (resolve_tac [exI,bexI] 1));
   14.21 @@ -59,7 +59,7 @@
   14.22  \ ==> EX K. EX NA. EX evs: recur lost.                          \
   14.23  \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
   14.24  \                  Agent Server|}                               \
   14.25 -\         : set_of_list evs";
   14.26 +\         : set evs";
   14.27  by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
   14.28  by (REPEAT (eresolve_tac [exE, conjE] 1));
   14.29  by (REPEAT (resolve_tac [exI,bexI] 1));
   14.30 @@ -87,7 +87,7 @@
   14.31  qed "recur_mono";
   14.32  
   14.33  (*Nobody sends themselves messages*)
   14.34 -goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set_of_list evs";
   14.35 +goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set evs";
   14.36  by (etac recur.induct 1);
   14.37  by (Auto_tac());
   14.38  qed_spec_mp "not_Says_to_self";
   14.39 @@ -126,7 +126,7 @@
   14.40  
   14.41  val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
   14.42  
   14.43 -goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set_of_list evs \
   14.44 +goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \
   14.45  \                ==> RA : analz (sees lost Spy evs)";
   14.46  by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   14.47  qed "RA4_analz_sees_Spy";
   14.48 @@ -382,7 +382,7 @@
   14.49  goal thy 
   14.50   "!!evs. evs : recur lost       \
   14.51  \ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \
   14.52 -\                  ~: set_of_list evs";
   14.53 +\                  ~: set evs";
   14.54  by (etac recur.induct 1);
   14.55  by (etac (respond.induct) 5);
   14.56  by (Auto_tac());
   14.57 @@ -530,7 +530,7 @@
   14.58  \             : parts (sees lost Spy evs);                        \
   14.59  \            A ~: lost;  evs : recur lost |]                        \
   14.60  \        ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|})  \
   14.61 -\             : set_of_list evs";
   14.62 +\             : set evs";
   14.63  by (etac rev_mp 1);
   14.64  by parts_induct_tac;
   14.65  by (Fake_parts_insert_tac 1);
   14.66 @@ -547,7 +547,7 @@
   14.67  goal thy 
   14.68   "!!evs. [| Crypt (shrK A) Y : parts (sees lost Spy evs);    \
   14.69  \           A ~: lost;  A ~= Spy;  evs : recur lost |]       \
   14.70 -\        ==> EX C RC. Says Server C RC : set_of_list evs &   \
   14.71 +\        ==> EX C RC. Says Server C RC : set evs &   \
   14.72  \                     Crypt (shrK A) Y : parts {RC}";
   14.73  by (etac rev_mp 1);
   14.74  by parts_induct_tac;
    15.1 --- a/src/HOL/Auth/Recur.thy	Thu Jun 26 11:58:05 1997 +0200
    15.2 +++ b/src/HOL/Auth/Recur.thy	Thu Jun 26 13:20:50 1997 +0200
    15.3 @@ -75,14 +75,14 @@
    15.4             NOTE: existing proofs don't need PA and are complicated by its
    15.5                  presence!  See parts_Fake_tac.*)
    15.6      RA2  "[| evs: recur lost;  B ~= C;  B ~= Server;  Nonce NB ~: used evs;
    15.7 -             Says A' B PA : set_of_list evs;  
    15.8 +             Says A' B PA : set evs;  
    15.9               PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
   15.10            ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
   15.11                # evs : recur lost"
   15.12  
   15.13           (*The Server receives Bob's message and prepares a response.*)
   15.14      RA3  "[| evs: recur lost;  B ~= Server;
   15.15 -             Says B' Server PB : set_of_list evs;
   15.16 +             Says B' Server PB : set evs;
   15.17               (PB,RB,K) : respond evs |]
   15.18            ==> Says Server B RB # evs : recur lost"
   15.19  
   15.20 @@ -91,11 +91,11 @@
   15.21      RA4  "[| evs: recur lost;  A ~= B;  
   15.22               Says B  C {|XH, Agent B, Agent C, Nonce NB, 
   15.23                           XA, Agent A, Agent B, Nonce NA, P|} 
   15.24 -               : set_of_list evs;
   15.25 +               : set evs;
   15.26               Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
   15.27                           Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
   15.28                           RA|}
   15.29 -               : set_of_list evs |]
   15.30 +               : set evs |]
   15.31            ==> Says B A RA # evs : recur lost"
   15.32  
   15.33  (**No "oops" message can readily be expressed, since each session key is
    16.1 --- a/src/HOL/Auth/Shared.ML	Thu Jun 26 11:58:05 1997 +0200
    16.2 +++ b/src/HOL/Auth/Shared.ML	Thu Jun 26 13:20:50 1997 +0200
    16.3 @@ -138,7 +138,7 @@
    16.4  				            setloop split_tac [expand_if]))));
    16.5  qed "UN_parts_sees_Says";
    16.6  
    16.7 -goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
    16.8 +goal thy "Says A B X : set evs --> X : sees lost Spy evs";
    16.9  by (list.induct_tac "evs" 1);
   16.10  by (Auto_tac ());
   16.11  qed_spec_mp "Says_imp_sees_Spy";
    17.1 --- a/src/HOL/Auth/WooLam.ML	Thu Jun 26 11:58:05 1997 +0200
    17.2 +++ b/src/HOL/Auth/WooLam.ML	Thu Jun 26 13:20:50 1997 +0200
    17.3 @@ -22,7 +22,7 @@
    17.4   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    17.5  \        ==> EX NB. EX evs: woolam.               \
    17.6  \               Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \
    17.7 -\                 : set_of_list evs";
    17.8 +\                 : set evs";
    17.9  by (REPEAT (resolve_tac [exI,bexI] 1));
   17.10  by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
   17.11            woolam.WL4 RS woolam.WL5) 2);
   17.12 @@ -35,7 +35,7 @@
   17.13  (**** Inductive proofs about woolam ****)
   17.14  
   17.15  (*Nobody sends themselves messages*)
   17.16 -goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set_of_list evs";
   17.17 +goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set evs";
   17.18  by (etac woolam.induct 1);
   17.19  by (Auto_tac());
   17.20  qed_spec_mp "not_Says_to_self";
   17.21 @@ -45,7 +45,7 @@
   17.22  
   17.23  (** For reasoning about the encrypted portion of messages **)
   17.24  
   17.25 -goal thy "!!evs. Says A' B X : set_of_list evs \
   17.26 +goal thy "!!evs. Says A' B X : set evs \
   17.27  \                ==> X : analz (sees lost Spy evs)";
   17.28  by (etac (Says_imp_sees_Spy RS analz.Inj) 1);
   17.29  qed "WL4_analz_sees_Spy";
   17.30 @@ -97,7 +97,7 @@
   17.31  goal thy 
   17.32   "!!evs. [| A ~: lost;  evs : woolam |]                   \
   17.33  \    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs)        \
   17.34 -\        --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)";
   17.35 +\        --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs)";
   17.36  by parts_induct_tac;
   17.37  by (Fake_parts_insert_tac 1);
   17.38  by (Blast_tac 1);
   17.39 @@ -109,8 +109,8 @@
   17.40  goal thy 
   17.41   "!!evs. [| A ~: lost;  evs : woolam;               \
   17.42  \           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
   17.43 -\            : set_of_list evs |]                                  \
   17.44 -\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
   17.45 +\            : set evs |]                                  \
   17.46 +\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
   17.47  by (blast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
   17.48                        addSEs [MPair_parts]
   17.49                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   17.50 @@ -122,9 +122,9 @@
   17.51  (*Server sent WL5 only if it received the right sort of message*)
   17.52  goal thy 
   17.53   "!!evs. evs : woolam ==>                                              \
   17.54 -\        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs   \
   17.55 +\        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs   \
   17.56  \        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
   17.57 -\               : set_of_list evs)";
   17.58 +\               : set evs)";
   17.59  by parts_induct_tac;
   17.60  by (Fake_parts_insert_tac 1);
   17.61  by (ALLGOALS Blast_tac);
   17.62 @@ -135,7 +135,7 @@
   17.63  goal thy 
   17.64   "!!evs. [| B ~: lost;  evs : woolam |]                   \
   17.65  \    ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)        \
   17.66 -\        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
   17.67 +\        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
   17.68  by parts_induct_tac;
   17.69  by (Fake_parts_insert_tac 1);
   17.70  qed_spec_mp "NB_Crypt_imp_Server_msg";
   17.71 @@ -143,9 +143,9 @@
   17.72  (*Partial guarantee for B: if it gets a message of correct form then the Server
   17.73    sent the same message.*)
   17.74  goal thy 
   17.75 - "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \
   17.76 + "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \
   17.77  \           B ~: lost;  evs : woolam |]                                  \
   17.78 -\        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
   17.79 +\        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
   17.80  by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   17.81                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   17.82  qed "B_got_WL5";
   17.83 @@ -155,9 +155,9 @@
   17.84    But A may have sent the nonce to some other agent and it could have reached
   17.85    the Server via the Spy.*)
   17.86  goal thy 
   17.87 - "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \
   17.88 + "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
   17.89  \           A ~: lost;  B ~: lost;  evs : woolam  |] \
   17.90 -\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
   17.91 +\        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
   17.92  by (blast_tac (!claset addIs  [Server_trusts_WL4]
   17.93                        addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
   17.94  qed "B_trusts_WL5";
   17.95 @@ -166,8 +166,8 @@
   17.96  (*B only issues challenges in response to WL1.  Useful??*)
   17.97  goal thy 
   17.98   "!!evs. [| B ~= Spy;  evs : woolam |]                   \
   17.99 -\    ==> Says B A (Nonce NB) : set_of_list evs        \
  17.100 -\        --> (EX A'. Says A' B (Agent A) : set_of_list evs)";
  17.101 +\    ==> Says B A (Nonce NB) : set evs        \
  17.102 +\        --> (EX A'. Says A' B (Agent A) : set evs)";
  17.103  by parts_induct_tac;
  17.104  by (Fake_parts_insert_tac 1);
  17.105  by (ALLGOALS Blast_tac);
  17.106 @@ -178,8 +178,8 @@
  17.107  goal thy 
  17.108   "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]                   \
  17.109  \    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) &  \
  17.110 -\        Says B A (Nonce NB) : set_of_list evs        \
  17.111 -\        --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
  17.112 +\        Says B A (Nonce NB) : set evs        \
  17.113 +\        --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
  17.114  by parts_induct_tac;
  17.115  by (Fake_parts_insert_tac 1);
  17.116  by (Step_tac 1);
    18.1 --- a/src/HOL/Auth/WooLam.thy	Thu Jun 26 11:58:05 1997 +0200
    18.2 +++ b/src/HOL/Auth/WooLam.thy	Thu Jun 26 13:20:50 1997 +0200
    18.3 @@ -36,27 +36,27 @@
    18.4  
    18.5           (*Bob responds to Alice's message with a challenge.*)
    18.6      WL2  "[| evs: woolam;  A ~= B;  
    18.7 -             Says A' B (Agent A) : set_of_list evs |]
    18.8 +             Says A' B (Agent A) : set evs |]
    18.9            ==> Says B A (Nonce NB) # evs : woolam"
   18.10  
   18.11           (*Alice responds to Bob's challenge by encrypting NB with her key.
   18.12             B is *not* properly determined -- Alice essentially broadcasts
   18.13             her reply.*)
   18.14      WL3  "[| evs: woolam;  A ~= B;
   18.15 -             Says A  B (Agent A)  : set_of_list evs;
   18.16 -             Says B' A (Nonce NB) : set_of_list evs |]
   18.17 +             Says A  B (Agent A)  : set evs;
   18.18 +             Says B' A (Nonce NB) : set evs |]
   18.19            ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
   18.20  
   18.21           (*Bob forwards Alice's response to the Server.*)
   18.22      WL4  "[| evs: woolam;  B ~= Server;  
   18.23 -             Says A'  B X         : set_of_list evs;
   18.24 -             Says A'' B (Agent A) : set_of_list evs |]
   18.25 +             Says A'  B X         : set evs;
   18.26 +             Says A'' B (Agent A) : set evs |]
   18.27            ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
   18.28  
   18.29           (*Server decrypts Alice's response for Bob.*)
   18.30      WL5  "[| evs: woolam;  B ~= Server;
   18.31               Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
   18.32 -               : set_of_list evs |]
   18.33 +               : set evs |]
   18.34            ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
   18.35                   # evs : woolam"
   18.36  
    19.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Jun 26 11:58:05 1997 +0200
    19.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Jun 26 13:20:50 1997 +0200
    19.3 @@ -24,7 +24,7 @@
    19.4  goal thy 
    19.5   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    19.6  \        ==> EX X NB K. EX evs: yahalom lost.          \
    19.7 -\               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
    19.8 +\               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    19.9  by (REPEAT (resolve_tac [exI,bexI] 1));
   19.10  by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
   19.11            yahalom.YM4) 2);
   19.12 @@ -45,7 +45,7 @@
   19.13  
   19.14  
   19.15  (*Nobody sends themselves messages*)
   19.16 -goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
   19.17 +goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
   19.18  by (etac yahalom.induct 1);
   19.19  by (Auto_tac());
   19.20  qed_spec_mp "not_Says_to_self";
   19.21 @@ -56,7 +56,7 @@
   19.22  (** For reasoning about the encrypted portion of messages **)
   19.23  
   19.24  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
   19.25 -goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \
   19.26 +goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
   19.27  \                X : analz (sees lost Spy evs)";
   19.28  by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
   19.29  qed "YM4_analz_sees_Spy";
   19.30 @@ -66,7 +66,7 @@
   19.31  
   19.32  (*Relates to both YM4 and Oops*)
   19.33  goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
   19.34 -\                  : set_of_list evs ==> \
   19.35 +\                  : set evs ==> \
   19.36  \                K : parts (sees lost Spy evs)";
   19.37  by (blast_tac (!claset addSEs partsEs
   19.38                        addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
   19.39 @@ -140,7 +140,7 @@
   19.40    Oops as well as main secrecy property.*)
   19.41  goal thy 
   19.42   "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
   19.43 -\             : set_of_list evs;                                           \
   19.44 +\             : set evs;                                           \
   19.45  \           evs : yahalom lost |]                                          \
   19.46  \        ==> K ~: range shrK";
   19.47  by (etac rev_mp 1);
   19.48 @@ -199,7 +199,7 @@
   19.49  \      EX A' B' na' nb' X'. ALL A B na nb X.                             \
   19.50  \          Says Server A                                            \
   19.51  \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
   19.52 -\          : set_of_list evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
   19.53 +\          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
   19.54  by (etac yahalom.induct 1);
   19.55  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   19.56  by (Step_tac 1);
   19.57 @@ -216,10 +216,10 @@
   19.58  goal thy 
   19.59  "!!evs. [| Says Server A                                            \
   19.60  \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
   19.61 -\           : set_of_list evs;                                      \
   19.62 +\           : set evs;                                      \
   19.63  \          Says Server A'                                           \
   19.64  \           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
   19.65 -\           : set_of_list evs;                                      \
   19.66 +\           : set evs;                                      \
   19.67  \          evs : yahalom lost |]                                    \
   19.68  \       ==> A=A' & B=B' & na=na' & nb=nb'";
   19.69  by (prove_unique_tac lemma 1);
   19.70 @@ -233,8 +233,8 @@
   19.71  \        ==> Says Server A                                        \
   19.72  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   19.73  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   19.74 -\             : set_of_list evs -->                               \
   19.75 -\            Says A Spy {|na, nb, Key K|} ~: set_of_list evs -->  \
   19.76 +\             : set evs -->                               \
   19.77 +\            Says A Spy {|na, nb, Key K|} ~: set evs -->  \
   19.78  \            Key K ~: analz (sees lost Spy evs)";
   19.79  by (etac yahalom.induct 1);
   19.80  by analz_sees_tac;
   19.81 @@ -259,8 +259,8 @@
   19.82   "!!evs. [| Says Server A                                         \
   19.83  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   19.84  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   19.85 -\             : set_of_list evs;                                  \
   19.86 -\           Says A Spy {|na, nb, Key K|} ~: set_of_list evs;      \
   19.87 +\             : set evs;                                  \
   19.88 +\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
   19.89  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   19.90  \        ==> Key K ~: analz (sees lost Spy evs)";
   19.91  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   19.92 @@ -274,8 +274,8 @@
   19.93  \           Says Server A                                         \
   19.94  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   19.95  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   19.96 -\             : set_of_list evs;                                  \
   19.97 -\           Says A Spy {|na, nb, Key K|} ~: set_of_list evs;      \
   19.98 +\             : set evs;                                  \
   19.99 +\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
  19.100  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
  19.101  \        ==> Key K ~: analz (sees lost C evs)";
  19.102  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
  19.103 @@ -309,7 +309,7 @@
  19.104  \         ==> Says Server A                                            \
  19.105  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
  19.106  \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
  19.107 -\             : set_of_list evs";
  19.108 +\             : set evs";
  19.109  by (etac rev_mp 1);
  19.110  by parts_induct_tac;
  19.111  by (Fake_parts_insert_tac 1);
  19.112 @@ -327,7 +327,7 @@
  19.113  \                        {|Crypt (shrK A) {|Agent B, Key K,             \
  19.114  \                                           Nonce NA, Nonce NB|},       \
  19.115  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
  19.116 -\                       : set_of_list evs";
  19.117 +\                       : set evs";
  19.118  by (etac rev_mp 1);
  19.119  by parts_induct_tac;
  19.120  by (Fake_parts_insert_tac 1);
  19.121 @@ -346,7 +346,7 @@
  19.122  \                        {|Crypt (shrK A) {|Agent B, Key K,             \
  19.123  \                                  Nonce NA, Nonce NB|},                \
  19.124  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
  19.125 -\                       : set_of_list evs)";
  19.126 +\                       : set evs)";
  19.127  by analz_mono_parts_induct_tac;
  19.128  (*YM3 & Fake*)
  19.129  by (Blast_tac 2);
  19.130 @@ -368,7 +368,7 @@
  19.131  goalw thy [KeyWithNonce_def]
  19.132   "!!evs. Says Server A                                              \
  19.133  \            {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
  19.134 -\          : set_of_list evs ==> KeyWithNonce K NB evs";
  19.135 +\          : set evs ==> KeyWithNonce K NB evs";
  19.136  by (Blast_tac 1);
  19.137  qed "KeyWithNonceI";
  19.138  
  19.139 @@ -394,7 +394,7 @@
  19.140  goalw thy [KeyWithNonce_def]
  19.141   "!!evs. [| Says Server A                                                \
  19.142  \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
  19.143 -\             : set_of_list evs;                                         \
  19.144 +\             : set evs;                                         \
  19.145  \           NB ~= NB';  evs : yahalom lost |]                            \
  19.146  \        ==> ~ KeyWithNonce K NB evs";
  19.147  by (blast_tac (!claset addDs [unique_session_keys]) 1);
  19.148 @@ -453,7 +453,7 @@
  19.149  goal thy 
  19.150   "!!evs. [| Says Server A                                                 \
  19.151  \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
  19.152 -\           : set_of_list evs;                                            \
  19.153 +\           : set evs;                                            \
  19.154  \           NB ~= NB';  KAB ~: range shrK;  evs : yahalom lost |]         \
  19.155  \        ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) =  \
  19.156  \            (Nonce NB : analz (sees lost Spy evs))";
  19.157 @@ -495,9 +495,9 @@
  19.158    not_lost_tac to remove the assumption B' ~: lost.*)
  19.159  goal thy 
  19.160   "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|}    \
  19.161 -\            : set_of_list evs;  B ~: lost;                               \
  19.162 +\            : set evs;  B ~: lost;                               \
  19.163  \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
  19.164 -\            : set_of_list evs;                                           \
  19.165 +\            : set evs;                                           \
  19.166  \          NB ~: analz (sees lost Spy evs);  evs : yahalom lost |]        \
  19.167  \        ==> NA' = NA & A' = A & B' = B";
  19.168  by (not_lost_tac "B'" 1);
  19.169 @@ -528,11 +528,11 @@
  19.170  (*The Server sends YM3 only in response to YM2.*)
  19.171  goal thy 
  19.172   "!!evs. [| Says Server A                                           \
  19.173 -\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \
  19.174 +\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs; \
  19.175  \           evs : yahalom lost |]                                        \
  19.176  \        ==> EX B'. Says B' Server                                       \
  19.177  \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
  19.178 -\                   : set_of_list evs";
  19.179 +\                   : set evs";
  19.180  by (etac rev_mp 1);
  19.181  by (etac yahalom.induct 1);
  19.182  by (ALLGOALS Asm_simp_tac);
  19.183 @@ -546,8 +546,8 @@
  19.184   "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
  19.185  \ ==> Says B Server                                                    \
  19.186  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
  19.187 -\     : set_of_list evs -->                               \
  19.188 -\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) -->  \
  19.189 +\     : set evs -->                               \
  19.190 +\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->  \
  19.191  \     Nonce NB ~: analz (sees lost Spy evs)";
  19.192  by (etac yahalom.induct 1);
  19.193  by analz_sees_tac;
  19.194 @@ -606,16 +606,16 @@
  19.195  goal thy 
  19.196   "!!evs. [| Says B Server                                                   \
  19.197  \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
  19.198 -\             : set_of_list evs;                                            \
  19.199 +\             : set evs;                                            \
  19.200  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
  19.201 -\                       Crypt K (Nonce NB)|} : set_of_list evs;             \
  19.202 -\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
  19.203 +\                       Crypt K (Nonce NB)|} : set evs;             \
  19.204 +\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \
  19.205  \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
  19.206  \         ==> Says Server A                                                 \
  19.207  \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
  19.208  \                               Nonce NA, Nonce NB|},                       \
  19.209  \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
  19.210 -\               : set_of_list evs";
  19.211 +\               : set evs";
  19.212  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
  19.213  by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1 THEN
  19.214      dtac B_trusts_YM4_shrK 1);
  19.215 @@ -638,7 +638,7 @@
  19.216  \      B ~: lost -->                                                   \
  19.217  \      Says B Server {|Agent B,                                \
  19.218  \                          Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
  19.219 -\         : set_of_list evs";
  19.220 +\         : set evs";
  19.221  by parts_induct_tac;
  19.222  by (Fake_parts_insert_tac 1);
  19.223  bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
  19.224 @@ -647,11 +647,11 @@
  19.225  goal thy 
  19.226   "!!evs. evs : yahalom lost                                       \
  19.227  \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
  19.228 -\         : set_of_list evs -->                                          \
  19.229 +\         : set evs -->                                          \
  19.230  \      B ~: lost -->                                                     \
  19.231  \      Says B Server {|Agent B,                            \
  19.232  \                               Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}   \
  19.233 -\                 : set_of_list evs";
  19.234 +\                 : set evs";
  19.235  by (etac yahalom.induct 1);
  19.236  by (ALLGOALS Asm_simp_tac);
  19.237  (*YM4*)
  19.238 @@ -664,10 +664,10 @@
  19.239  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
  19.240  goal thy
  19.241   "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
  19.242 -\             : set_of_list evs;                                            \
  19.243 +\             : set evs;                                            \
  19.244  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
  19.245  \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
  19.246 -\         : set_of_list evs";
  19.247 +\         : set evs";
  19.248  by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
  19.249  		       addEs sees_Spy_partsEs) 1);
  19.250  qed "YM3_auth_B_to_A";
  19.251 @@ -698,7 +698,7 @@
  19.252  \            Crypt (shrK B) {|Agent A, Key K|}                          \
  19.253  \              : parts (sees lost Spy evs) -->                          \
  19.254  \            B ~: lost -->                                              \
  19.255 -\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs)";
  19.256 +\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
  19.257  by analz_mono_parts_induct_tac;
  19.258  (*Fake*)
  19.259  by (Fake_parts_insert_tac 1);
  19.260 @@ -720,13 +720,13 @@
  19.261  goal thy 
  19.262   "!!evs. [| Says B Server                                                   \
  19.263  \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
  19.264 -\             : set_of_list evs;                                            \
  19.265 +\             : set evs;                                            \
  19.266  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},       \
  19.267 -\                       Crypt K (Nonce NB)|} : set_of_list evs;  \
  19.268 +\                       Crypt K (Nonce NB)|} : set evs;  \
  19.269  \           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|}    \
  19.270 -\               ~: set_of_list evs);                             \
  19.271 +\               ~: set evs);                             \
  19.272  \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
  19.273 -\        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
  19.274 +\        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
  19.275  by (dtac B_trusts_YM4 1);
  19.276  by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
  19.277  by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
    20.1 --- a/src/HOL/Auth/Yahalom.thy	Thu Jun 26 11:58:05 1997 +0200
    20.2 +++ b/src/HOL/Auth/Yahalom.thy	Thu Jun 26 13:20:50 1997 +0200
    20.3 @@ -32,7 +32,7 @@
    20.4           (*Bob's response to Alice's message.  Bob doesn't know who 
    20.5  	   the sender is, hence the A' in the sender field.*)
    20.6      YM2  "[| evs: yahalom lost;  B ~= Server;  Nonce NB ~: used evs;
    20.7 -             Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    20.8 +             Says A' B {|Agent A, Nonce NA|} : set evs |]
    20.9            ==> Says B Server 
   20.10                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   20.11                  # evs : yahalom lost"
   20.12 @@ -42,7 +42,7 @@
   20.13      YM3  "[| evs: yahalom lost;  A ~= Server;  Key KAB ~: used evs;
   20.14               Says B' Server 
   20.15                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   20.16 -               : set_of_list evs |]
   20.17 +               : set evs |]
   20.18            ==> Says Server A
   20.19                     {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
   20.20                       Crypt (shrK B) {|Agent A, Key KAB|}|}
   20.21 @@ -52,8 +52,8 @@
   20.22             uses the new session key to send Bob his Nonce.*)
   20.23      YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
   20.24               Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
   20.25 -                        X|}  : set_of_list evs;
   20.26 -             Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
   20.27 +                        X|}  : set evs;
   20.28 +             Says A B {|Agent A, Nonce NA|} : set evs |]
   20.29            ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
   20.30  
   20.31           (*This message models possible leaks of session keys.  The Nonces
   20.32 @@ -62,7 +62,7 @@
   20.33      Oops "[| evs: yahalom lost;  A ~= Spy;
   20.34               Says Server A {|Crypt (shrK A)
   20.35                                     {|Agent B, Key K, Nonce NA, Nonce NB|},
   20.36 -                             X|}  : set_of_list evs |]
   20.37 +                             X|}  : set evs |]
   20.38            ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
   20.39  
   20.40  
   20.41 @@ -71,6 +71,6 @@
   20.42    "KeyWithNonce K NB evs ==
   20.43       EX A B na X. 
   20.44         Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} 
   20.45 -         : set_of_list evs"
   20.46 +         : set evs"
   20.47  
   20.48  end
    21.1 --- a/src/HOL/Auth/Yahalom2.ML	Thu Jun 26 11:58:05 1997 +0200
    21.2 +++ b/src/HOL/Auth/Yahalom2.ML	Thu Jun 26 13:20:50 1997 +0200
    21.3 @@ -25,7 +25,7 @@
    21.4  goal thy 
    21.5   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    21.6  \        ==> EX X NB K. EX evs: yahalom lost.          \
    21.7 -\               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
    21.8 +\               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    21.9  by (REPEAT (resolve_tac [exI,bexI] 1));
   21.10  by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
   21.11            yahalom.YM4) 2);
   21.12 @@ -46,7 +46,7 @@
   21.13  
   21.14  
   21.15  (*Nobody sends themselves messages*)
   21.16 -goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
   21.17 +goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
   21.18  by (etac yahalom.induct 1);
   21.19  by (Auto_tac());
   21.20  qed_spec_mp "not_Says_to_self";
   21.21 @@ -57,7 +57,7 @@
   21.22  (** For reasoning about the encrypted portion of messages **)
   21.23  
   21.24  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
   21.25 -goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set_of_list evs ==> \
   21.26 +goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \
   21.27  \                X : analz (sees lost Spy evs)";
   21.28  by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
   21.29  qed "YM4_analz_sees_Spy";
   21.30 @@ -67,7 +67,7 @@
   21.31  
   21.32  (*Relates to both YM4 and Oops*)
   21.33  goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \
   21.34 -\                  : set_of_list evs ==> \
   21.35 +\                  : set evs ==> \
   21.36  \                K : parts (sees lost Spy evs)";
   21.37  by (blast_tac (!claset addSEs partsEs
   21.38                        addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
   21.39 @@ -140,7 +140,7 @@
   21.40    Oops as well as main secrecy property.*)
   21.41  goal thy 
   21.42   "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \
   21.43 -\            : set_of_list evs;                                         \
   21.44 +\            : set evs;                                         \
   21.45  \           evs : yahalom lost |]                                       \
   21.46  \        ==> K ~: range shrK & A ~= B";
   21.47  by (etac rev_mp 1);
   21.48 @@ -200,7 +200,7 @@
   21.49  \      EX A' B' na' nb' X'. ALL A B na nb X.                        \
   21.50  \          Says Server A                                            \
   21.51  \           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}        \
   21.52 -\          : set_of_list evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
   21.53 +\          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
   21.54  by (etac yahalom.induct 1);
   21.55  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   21.56  by (Step_tac 1);
   21.57 @@ -216,10 +216,10 @@
   21.58  goal thy 
   21.59  "!!evs. [| Says Server A                                            \
   21.60  \           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}        \
   21.61 -\           : set_of_list evs;                                      \
   21.62 +\           : set evs;                                      \
   21.63  \          Says Server A'                                           \
   21.64  \           {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|}   \
   21.65 -\           : set_of_list evs;                                      \
   21.66 +\           : set evs;                                      \
   21.67  \          evs : yahalom lost |]                                    \
   21.68  \       ==> A=A' & B=B' & na=na' & nb=nb'";
   21.69  by (prove_unique_tac lemma 1);
   21.70 @@ -234,8 +234,8 @@
   21.71  \        ==> Says Server A                                           \
   21.72  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},          \
   21.73  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}         \
   21.74 -\             : set_of_list evs -->                                  \
   21.75 -\            Says A Spy {|na, nb, Key K|} ~: set_of_list evs -->     \
   21.76 +\             : set evs -->                                  \
   21.77 +\            Says A Spy {|na, nb, Key K|} ~: set evs -->     \
   21.78  \            Key K ~: analz (sees lost Spy evs)";
   21.79  by (etac yahalom.induct 1);
   21.80  by analz_sees_tac;
   21.81 @@ -260,8 +260,8 @@
   21.82   "!!evs. [| Says Server A                                         \
   21.83  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
   21.84  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
   21.85 -\           : set_of_list evs;                                    \
   21.86 -\           Says A Spy {|na, nb, Key K|} ~: set_of_list evs;      \
   21.87 +\           : set evs;                                    \
   21.88 +\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
   21.89  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   21.90  \        ==> Key K ~: analz (sees lost Spy evs)";
   21.91  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   21.92 @@ -275,8 +275,8 @@
   21.93  \           Says Server A                                         \
   21.94  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
   21.95  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
   21.96 -\           : set_of_list evs;                                    \
   21.97 -\           Says A Spy {|na, nb, Key K|} ~: set_of_list evs;      \
   21.98 +\           : set evs;                                    \
   21.99 +\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
  21.100  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
  21.101  \        ==> Key K ~: analz (sees lost C evs)";
  21.102  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
  21.103 @@ -297,7 +297,7 @@
  21.104  \         ==> EX nb. Says Server A                                     \
  21.105  \                      {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
  21.106  \                            Crypt (shrK B) {|nb, Key K, Agent A|}|}   \
  21.107 -\                    : set_of_list evs";
  21.108 +\                    : set evs";
  21.109  by (etac rev_mp 1);
  21.110  by parts_induct_tac;
  21.111  by (Fake_parts_insert_tac 1);
  21.112 @@ -317,7 +317,7 @@
  21.113  \                    {|Nonce NB,                                     \
  21.114  \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},  \
  21.115  \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
  21.116 -\                       : set_of_list evs";
  21.117 +\                       : set evs";
  21.118  by (etac rev_mp 1);
  21.119  by parts_induct_tac;
  21.120  by (Fake_parts_insert_tac 1);
  21.121 @@ -333,13 +333,13 @@
  21.122    because we do not have to show that NB is secret. *)
  21.123  goal thy 
  21.124   "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
  21.125 -\             : set_of_list evs;                                         \
  21.126 +\             : set evs;                                         \
  21.127  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                \
  21.128  \        ==> EX NA. Says Server A                                        \
  21.129  \                    {|Nonce NB,                                         \
  21.130  \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},      \
  21.131  \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}     \
  21.132 -\                   : set_of_list evs";
  21.133 +\                   : set evs";
  21.134  by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
  21.135  by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
  21.136  qed "B_trusts_YM4";
  21.137 @@ -355,7 +355,7 @@
  21.138  \      B ~: lost -->                                                   \
  21.139  \      (EX NB. Says B Server {|Agent B, Nonce NB,                      \
  21.140  \                              Crypt (shrK B) {|Agent A, Nonce NA|}|}  \
  21.141 -\         : set_of_list evs)";
  21.142 +\         : set evs)";
  21.143  by parts_induct_tac;
  21.144  by (Fake_parts_insert_tac 1);
  21.145  (*YM2*)
  21.146 @@ -366,11 +366,11 @@
  21.147  goal thy 
  21.148   "!!evs. evs : yahalom lost                                       \
  21.149  \  ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
  21.150 -\         : set_of_list evs -->                                          \
  21.151 +\         : set evs -->                                          \
  21.152  \      B ~: lost -->                                                     \
  21.153  \      (EX nb'. Says B Server {|Agent B, nb',                            \
  21.154  \                               Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
  21.155 -\                 : set_of_list evs)";
  21.156 +\                 : set evs)";
  21.157  by (etac yahalom.induct 1);
  21.158  by (ALLGOALS Asm_simp_tac);
  21.159  (*YM3*)
  21.160 @@ -384,11 +384,11 @@
  21.161  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
  21.162  goal thy
  21.163   "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
  21.164 -\             : set_of_list evs;                                            \
  21.165 +\             : set evs;                                            \
  21.166  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
  21.167  \   ==> EX nb'. Says B Server                                               \
  21.168  \                    {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
  21.169 -\                 : set_of_list evs";
  21.170 +\                 : set evs";
  21.171  by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
  21.172  		       addEs sees_Spy_partsEs) 1);
  21.173  qed "YM3_auth_B_to_A";
  21.174 @@ -419,7 +419,7 @@
  21.175  \            Crypt (shrK B) {|Nonce NB, Key K, Agent A|}                \
  21.176  \              : parts (sees lost Spy evs) -->                          \
  21.177  \            B ~: lost -->                                              \
  21.178 -\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs)";
  21.179 +\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
  21.180  by analz_mono_parts_induct_tac;
  21.181  (*Fake*)
  21.182  by (Fake_parts_insert_tac 1);
  21.183 @@ -440,11 +440,10 @@
  21.184    Other premises guarantee secrecy of K.*)
  21.185  goal thy 
  21.186   "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
  21.187 -\                       Crypt K (Nonce NB)|} : set_of_list evs;         \
  21.188 -\           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|}           \
  21.189 -\               ~: set_of_list evs);                                    \
  21.190 +\                       Crypt K (Nonce NB)|} : set evs;         \
  21.191 +\           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
  21.192  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
  21.193 -\        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
  21.194 +\        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
  21.195  by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
  21.196  by (dtac B_trusts_YM4_shrK 1);
  21.197  by (safe_tac (!claset));
    22.1 --- a/src/HOL/Auth/Yahalom2.thy	Thu Jun 26 11:58:05 1997 +0200
    22.2 +++ b/src/HOL/Auth/Yahalom2.thy	Thu Jun 26 13:20:50 1997 +0200
    22.3 @@ -35,7 +35,7 @@
    22.4           (*Bob's response to Alice's message.  Bob doesn't know who 
    22.5  	   the sender is, hence the A' in the sender field.*)
    22.6      YM2  "[| evs: yahalom lost;  B ~= Server;  Nonce NB ~: used evs;
    22.7 -             Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    22.8 +             Says A' B {|Agent A, Nonce NA|} : set evs |]
    22.9            ==> Says B Server 
   22.10                    {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
   22.11                  # evs : yahalom lost"
   22.12 @@ -46,7 +46,7 @@
   22.13      YM3  "[| evs: yahalom lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
   22.14               Says B' Server {|Agent B, Nonce NB,
   22.15  			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
   22.16 -               : set_of_list evs |]
   22.17 +               : set evs |]
   22.18            ==> Says Server A
   22.19                 {|Nonce NB, 
   22.20                   Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
   22.21 @@ -58,8 +58,8 @@
   22.22      YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
   22.23               Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   22.24                          X|}
   22.25 -               : set_of_list evs;
   22.26 -             Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
   22.27 +               : set evs;
   22.28 +             Says A B {|Agent A, Nonce NA|} : set evs |]
   22.29            ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
   22.30  
   22.31           (*This message models possible leaks of session keys.  The nonces
   22.32 @@ -68,7 +68,7 @@
   22.33      Oops "[| evs: yahalom lost;  A ~= Spy;
   22.34               Says Server A {|Nonce NB, 
   22.35                               Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   22.36 -                             X|}  : set_of_list evs |]
   22.37 +                             X|}  : set evs |]
   22.38            ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
   22.39  
   22.40  end
    23.1 --- a/src/HOL/List.ML	Thu Jun 26 11:58:05 1997 +0200
    23.2 +++ b/src/HOL/List.ML	Thu Jun 26 13:20:50 1997 +0200
    23.3 @@ -112,7 +112,7 @@
    23.4  (** map **)
    23.5  
    23.6  goal thy
    23.7 -  "(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs";
    23.8 +  "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
    23.9  by (induct_tac "xs" 1);
   23.10  by (ALLGOALS Asm_simp_tac);
   23.11  bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
   23.12 @@ -170,38 +170,38 @@
   23.13  qed "mem_filter";
   23.14  Addsimps[mem_filter];
   23.15  
   23.16 -(** set_of_list **)
   23.17 +(** set **)
   23.18  
   23.19 -goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
   23.20 +goal thy "set (xs@ys) = (set xs Un set ys)";
   23.21  by (induct_tac "xs" 1);
   23.22  by (ALLGOALS Asm_simp_tac);
   23.23  qed "set_of_list_append";
   23.24  Addsimps[set_of_list_append];
   23.25  
   23.26 -goal thy "(x mem xs) = (x: set_of_list xs)";
   23.27 +goal thy "(x mem xs) = (x: set xs)";
   23.28  by (induct_tac "xs" 1);
   23.29  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   23.30  by (Blast_tac 1);
   23.31  qed "set_of_list_mem_eq";
   23.32  
   23.33 -goal thy "set_of_list l <= set_of_list (x#l)";
   23.34 +goal thy "set l <= set (x#l)";
   23.35  by (Simp_tac 1);
   23.36  by (Blast_tac 1);
   23.37  qed "set_of_list_subset_Cons";
   23.38  
   23.39 -goal thy "(set_of_list xs = {}) = (xs = [])";
   23.40 +goal thy "(set xs = {}) = (xs = [])";
   23.41  by (induct_tac "xs" 1);
   23.42  by (ALLGOALS Asm_simp_tac);
   23.43  qed "set_of_list_empty";
   23.44  Addsimps [set_of_list_empty];
   23.45  
   23.46 -goal thy "set_of_list(rev xs) = set_of_list(xs)";
   23.47 +goal thy "set(rev xs) = set(xs)";
   23.48  by (induct_tac "xs" 1);
   23.49  by (ALLGOALS Asm_simp_tac);
   23.50  qed "set_of_list_rev";
   23.51  Addsimps [set_of_list_rev];
   23.52  
   23.53 -goal thy "set_of_list(map f xs) = f``(set_of_list xs)";
   23.54 +goal thy "set(map f xs) = f``(set xs)";
   23.55  by (induct_tac "xs" 1);
   23.56  by (ALLGOALS Asm_simp_tac);
   23.57  qed "set_of_list_map";
   23.58 @@ -483,7 +483,7 @@
   23.59  (** takeWhile & dropWhile **)
   23.60  
   23.61  goal thy
   23.62 -  "x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
   23.63 +  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
   23.64  by (induct_tac "xs" 1);
   23.65   by (Simp_tac 1);
   23.66  by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   23.67 @@ -492,7 +492,7 @@
   23.68  Addsimps [takeWhile_append1];
   23.69  
   23.70  goal thy
   23.71 -  "(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
   23.72 +  "(!x:set xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
   23.73  by (induct_tac "xs" 1);
   23.74   by (Simp_tac 1);
   23.75  by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   23.76 @@ -500,7 +500,7 @@
   23.77  Addsimps [takeWhile_append2];
   23.78  
   23.79  goal thy
   23.80 -  "x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
   23.81 +  "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
   23.82  by (induct_tac "xs" 1);
   23.83   by (Simp_tac 1);
   23.84  by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   23.85 @@ -509,14 +509,14 @@
   23.86  Addsimps [dropWhile_append1];
   23.87  
   23.88  goal thy
   23.89 -  "(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
   23.90 +  "(!x:set xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
   23.91  by (induct_tac "xs" 1);
   23.92   by (Simp_tac 1);
   23.93  by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   23.94  bind_thm("dropWhile_append2", ballI RS (result() RS mp));
   23.95  Addsimps [dropWhile_append2];
   23.96  
   23.97 -goal thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x";
   23.98 +goal thy "x:set(takeWhile P xs) --> x:set xs & P x";
   23.99  by (induct_tac "xs" 1);
  23.100   by (Simp_tac 1);
  23.101  by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    24.1 --- a/src/HOL/List.thy	Thu Jun 26 11:58:05 1997 +0200
    24.2 +++ b/src/HOL/List.thy	Thu Jun 26 13:20:50 1997 +0200
    24.3 @@ -16,7 +16,7 @@
    24.4    concat      :: 'a list list => 'a list
    24.5    foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
    24.6    hd          :: 'a list => 'a
    24.7 -  set_of_list :: 'a list => 'a set
    24.8 +  set         :: 'a list => 'a set
    24.9    list_all    :: ('a => bool) => ('a list => bool)
   24.10    map         :: ('a=>'b) => ('a list => 'b list)
   24.11    mem         :: ['a, 'a list] => bool                    (infixl 55)
   24.12 @@ -70,9 +70,9 @@
   24.13  primrec "op mem" list
   24.14    "x mem [] = False"
   24.15    "x mem (y#ys) = (if y=x then True else x mem ys)"
   24.16 -primrec set_of_list list
   24.17 -  "set_of_list [] = {}"
   24.18 -  "set_of_list (x#xs) = insert x (set_of_list xs)"
   24.19 +primrec set list
   24.20 +  "set [] = {}"
   24.21 +  "set (x#xs) = insert x (set xs)"
   24.22  primrec list_all list
   24.23    list_all_Nil  "list_all P [] = True"
   24.24    list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
    25.1 --- a/src/HOL/ex/InSort.ML	Thu Jun 26 11:58:05 1997 +0200
    25.2 +++ b/src/HOL/ex/InSort.ML	Thu Jun 26 13:20:50 1997 +0200
    25.3 @@ -18,7 +18,7 @@
    25.4  by (ALLGOALS Asm_simp_tac);
    25.5  qed "insort_permutes";
    25.6  
    25.7 -goal thy "set_of_list(ins f x xs) = insert x (set_of_list xs)";
    25.8 +goal thy "set(ins f x xs) = insert x (set xs)";
    25.9  by (asm_simp_tac (!simpset addsimps [set_of_list_via_mset]
   25.10                             setloop (split_tac [expand_if])) 1);
   25.11  by (Fast_tac 1);
    26.1 --- a/src/HOL/ex/Qsort.ML	Thu Jun 26 11:58:05 1997 +0200
    26.2 +++ b/src/HOL/ex/Qsort.ML	Thu Jun 26 13:20:50 1997 +0200
    26.3 @@ -29,13 +29,13 @@
    26.4  by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    26.5  qed "qsort_permutes";
    26.6  
    26.7 -goal Qsort.thy "set_of_list(qsort le xs) = set_of_list xs";
    26.8 +goal Qsort.thy "set(qsort le xs) = set xs";
    26.9  by(simp_tac (!simpset addsimps [set_of_list_via_mset,qsort_permutes]) 1);
   26.10  qed "set_of_list_qsort";
   26.11  Addsimps [set_of_list_qsort];
   26.12  
   26.13  goal List.thy
   26.14 -  "(!x:set_of_list[x:xs.P(x)].Q(x)) = (!x:set_of_list xs. P(x)-->Q(x))";
   26.15 +  "(!x:set[x:xs.P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
   26.16  by (list.induct_tac "xs" 1);
   26.17  by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   26.18  qed"Ball_set_of_list_filter";
   26.19 @@ -43,7 +43,7 @@
   26.20  
   26.21  goal Qsort.thy
   26.22   "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
   26.23 -\                     (!x:set_of_list xs. !y:set_of_list ys. le x y))";
   26.24 +\                     (!x:set xs. !y:set ys. le x y))";
   26.25  by (list.induct_tac "xs" 1);
   26.26  by (ALLGOALS Asm_simp_tac);
   26.27  qed "sorted_append";
    27.1 --- a/src/HOL/ex/Sorting.ML	Thu Jun 26 11:58:05 1997 +0200
    27.2 +++ b/src/HOL/ex/Sorting.ML	Thu Jun 26 13:20:50 1997 +0200
    27.3 @@ -19,7 +19,7 @@
    27.4  
    27.5  Addsimps [mset_append, mset_compl_add];
    27.6  
    27.7 -goal Sorting.thy "set_of_list xs = {x.mset xs x ~= 0}";
    27.8 +goal Sorting.thy "set xs = {x.mset xs x ~= 0}";
    27.9  by (list.induct_tac "xs" 1);
   27.10  by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   27.11  by (Fast_tac 1);
    28.1 --- a/src/HOL/ex/Sorting.thy	Thu Jun 26 11:58:05 1997 +0200
    28.2 +++ b/src/HOL/ex/Sorting.thy	Thu Jun 26 13:20:50 1997 +0200
    28.3 @@ -21,7 +21,7 @@
    28.4  
    28.5  primrec sorted list
    28.6    "sorted le [] = True"
    28.7 -  "sorted le (x#xs) = ((!y:set_of_list xs. le x y) & sorted le xs)"
    28.8 +  "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
    28.9  
   28.10  primrec mset list
   28.11    "mset [] y = 0"