# HG changeset patch
# User wenzelm
# Date 1451340813 -3600
# Node ID 38b73f7940af1764e1aa3e42e54ee8033fdea9dc
# Parent  e96292f32c3cfae42a5941dabdb21d2ae4d25a6c
more symbols;

diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/CertifiedEmail.thy
--- a/src/HOL/Auth/CertifiedEmail.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/CertifiedEmail.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -25,7 +25,7 @@
 
 text\<open>We formalize a fixed way of computing responses.  Could be better.\<close>
 definition "response" :: "agent => agent => nat => msg" where
-   "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}"
+   "response S R q == Hash \<lbrace>Agent S, Key (shrK R), Nonce q\<rbrace>"
 
 
 inductive_set certified_mail :: "event list set"
@@ -42,28 +42,28 @@
 | FakeSSL: \<comment>\<open>The Spy may open SSL sessions with TTP, who is the only agent
     equipped with the necessary credentials to serve as an SSL server.\<close>
          "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|]
-          ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"
+          ==> Notes TTP \<lbrace>Agent Spy, Agent TTP, X\<rbrace> # evsfssl \<in> certified_mail"
 
 | CM1: \<comment>\<open>The sender approaches the recipient.  The message is a number.\<close>
  "[|evs1 \<in> certified_mail;
     Key K \<notin> used evs1;
     K \<in> symKeys;
     Nonce q \<notin> used evs1;
-    hs = Hash{|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
-    S2TTP = Crypt(pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
-  ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 
-                 Number cleartext, Nonce q, S2TTP|} # evs1 
+    hs = Hash\<lbrace>Number cleartext, Nonce q, response S R q, Crypt K (Number m)\<rbrace>;
+    S2TTP = Crypt(pubEK TTP) \<lbrace>Agent S, Number BothAuth, Key K, Agent R, hs\<rbrace>|]
+  ==> Says S R \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 
+                 Number cleartext, Nonce q, S2TTP\<rbrace> # evs1 
         \<in> certified_mail"
 
 | CM2: \<comment>\<open>The recipient records @{term S2TTP} while transmitting it and her
      password to @{term TTP} over an SSL channel.\<close>
  "[|evs2 \<in> certified_mail;
-    Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, 
-             Nonce q, S2TTP|} \<in> set evs2;
+    Gets R \<lbrace>Agent S, Agent TTP, em, Number BothAuth, Number cleartext, 
+             Nonce q, S2TTP\<rbrace> \<in> set evs2;
     TTP \<noteq> R;  
-    hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |]
+    hr = Hash \<lbrace>Number cleartext, Nonce q, response S R q, em\<rbrace> |]
   ==> 
-   Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2
+   Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, Key(RPwd R), hr\<rbrace> # evs2
       \<in> certified_mail"
 
 | CM3: \<comment>\<open>@{term TTP} simultaneously reveals the key to the recipient and gives
@@ -72,12 +72,12 @@
          if the given password is that of the claimed sender, @{term R}.
          He replies over the established SSL channel.\<close>
  "[|evs3 \<in> certified_mail;
-    Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} \<in> set evs3;
+    Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, Key(RPwd R), hr\<rbrace> \<in> set evs3;
     S2TTP = Crypt (pubEK TTP) 
-                     {|Agent S, Number BothAuth, Key k, Agent R, hs|};
+                     \<lbrace>Agent S, Number BothAuth, Key k, Agent R, hs\<rbrace>;
     TTP \<noteq> R;  hs = hr;  k \<in> symKeys|]
   ==> 
-   Notes R {|Agent TTP, Agent R, Key k, hr|} # 
+   Notes R \<lbrace>Agent TTP, Agent R, Key k, hr\<rbrace> # 
    Gets S (Crypt (priSK TTP) S2TTP) # 
    Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \<in> certified_mail"
 
@@ -116,8 +116,8 @@
 done
 
 lemma CM2_S2TTP_analz_knows_Spy:
- "[|Gets R {|Agent A, Agent B, em, Number AO, Number cleartext, 
-              Nonce q, S2TTP|} \<in> set evs;
+ "[|Gets R \<lbrace>Agent A, Agent B, em, Number AO, Number cleartext, 
+              Nonce q, S2TTP\<rbrace> \<in> set evs;
     evs \<in> certified_mail|] 
   ==> S2TTP \<in> analz(spies evs)"
 apply (drule Gets_imp_Says, simp) 
@@ -130,9 +130,9 @@
 lemma hr_form_lemma [rule_format]:
  "evs \<in> certified_mail
   ==> hr \<notin> synth (analz (spies evs)) --> 
-      (\<forall>S2TTP. Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|}
+      (\<forall>S2TTP. Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, pwd, hr\<rbrace>
           \<in> set evs --> 
-      (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|}))"
+      (\<exists>clt q S em. hr = Hash \<lbrace>Number clt, Nonce q, response S R q, em\<rbrace>))"
 apply (erule certified_mail.induct)
 apply (synth_analz_mono_contra, simp_all, blast+)
 done 
@@ -141,10 +141,10 @@
 the fakessl rule allows Spy to spoof the sender's name.  Maybe can
 strengthen the second disjunct with @{term "R\<noteq>Spy"}.\<close>
 lemma hr_form:
- "[|Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|} \<in> set evs;
+ "[|Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, pwd, hr\<rbrace> \<in> set evs;
     evs \<in> certified_mail|]
   ==> hr \<in> synth (analz (spies evs)) | 
-      (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|})"
+      (\<exists>clt q S em. hr = Hash \<lbrace>Number clt, Nonce q, response S R q, em\<rbrace>)"
 by (blast intro: hr_form_lemma) 
 
 lemma Spy_dont_know_private_keys [dest!]:
@@ -184,9 +184,9 @@
 
 lemma CM3_k_parts_knows_Spy:
  "[| evs \<in> certified_mail;
-     Notes TTP {|Agent A, Agent TTP,
-                 Crypt (pubEK TTP) {|Agent S, Number AO, Key K, 
-                 Agent R, hs|}, Key (RPwd R), hs|} \<in> set evs|]
+     Notes TTP \<lbrace>Agent A, Agent TTP,
+                 Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, 
+                 Agent R, hs\<rbrace>, Key (RPwd R), hs\<rbrace> \<in> set evs|]
   ==> Key K \<in> parts(spies evs)"
 apply (rotate_tac 1)
 apply (erule rev_mp)
@@ -273,7 +273,7 @@
     provided @{term K} is secure.  Proof is surprisingly hard.\<close>
 
 lemma Notes_SSL_imp_used:
-     "[|Notes B {|Agent A, Agent B, X|} \<in> set evs|] ==> X \<in> used evs"
+     "[|Notes B \<lbrace>Agent A, Agent B, X\<rbrace> \<in> set evs|] ==> X \<in> used evs"
 by (blast dest!: Notes_imp_used)
 
 
@@ -283,14 +283,14 @@
  "evs \<in> certified_mail ==>
     Key K \<notin> analz (spies evs) -->
     (\<forall>AO. Crypt (pubEK TTP)
-           {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs -->
+           \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace> \<in> used evs -->
     (\<exists>m ctxt q. 
-        hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
+        hs = Hash\<lbrace>Number ctxt, Nonce q, response S R q, Crypt K (Number m)\<rbrace> &
         Says S R
-           {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+           \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
              Number ctxt, Nonce q,
              Crypt (pubEK TTP)
-              {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs))" 
+              \<lbrace>Agent S, Number AO, Key K, Agent R, hs \<rbrace>\<rbrace> \<in> set evs))" 
 apply (erule certified_mail.induct, analz_mono_contra)
 apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp)
 apply (simp add: used_Nil Crypt_notin_initState, simp_all)
@@ -310,16 +310,16 @@
 done 
 
 lemma S2TTP_sender:
- "[|Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
+ "[|Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace> \<in> used evs;
     Key K \<notin> analz (spies evs);
     evs \<in> certified_mail|]
   ==> \<exists>m ctxt q. 
-        hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
+        hs = Hash\<lbrace>Number ctxt, Nonce q, response S R q, Crypt K (Number m)\<rbrace> &
         Says S R
-           {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+           \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
              Number ctxt, Nonce q,
              Crypt (pubEK TTP)
-              {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs" 
+              \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>\<rbrace> \<in> set evs" 
 by (blast intro: S2TTP_sender_lemma) 
 
 
@@ -348,15 +348,15 @@
        Key K \<notin> analz (spies evs) -->
        (\<forall>m cleartext q hs.
         Says S R
-           {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+           \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
              Number cleartext, Nonce q,
-             Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}|}
+             Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>\<rbrace>
           \<in> set evs -->
        (\<forall>m' cleartext' q' hs'.
        Says S' R'
-           {|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
+           \<lbrace>Agent S', Agent TTP, Crypt K (Number m'), Number AO',
              Number cleartext', Nonce q',
-             Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
+             Crypt (pubEK TTP) \<lbrace>Agent S', Number AO', Key K, Agent R', hs'\<rbrace>\<rbrace>
           \<in> set evs --> R' = R & S' = S & AO' = AO & hs' = hs))" 
 apply (erule certified_mail.induct, analz_mono_contra, simp_all)
  prefer 2
@@ -369,14 +369,14 @@
 text\<open>The key determines the sender, recipient and protocol options.\<close>
 lemma Key_unique:
       "[|Says S R
-           {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+           \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
              Number cleartext, Nonce q,
-             Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}|}
+             Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>\<rbrace>
           \<in> set evs;
          Says S' R'
-           {|Agent S', Agent TTP, Crypt K (Number m'), Number AO',
+           \<lbrace>Agent S', Agent TTP, Crypt K (Number m'), Number AO',
              Number cleartext', Nonce q',
-             Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
+             Crypt (pubEK TTP) \<lbrace>Agent S', Number AO', Key K, Agent R', hs'\<rbrace>\<rbrace>
           \<in> set evs;
          Key K \<notin> analz (spies evs);
          evs \<in> certified_mail|]
@@ -390,9 +390,9 @@
       If Spy gets the key then @{term R} is bad and @{term S} moreover
       gets his return receipt (and therefore has no grounds for complaint).\<close>
 theorem S_fairness_bad_R:
-      "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
-                     Number cleartext, Nonce q, S2TTP|} \<in> set evs;
-         S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
+      "[|Says S R \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO, 
+                     Number cleartext, Nonce q, S2TTP\<rbrace> \<in> set evs;
+         S2TTP = Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>;
          Key K \<in> analz (spies evs);
          evs \<in> certified_mail;
          S\<noteq>Spy|]
@@ -418,9 +418,9 @@
 
 text\<open>Confidentially for the symmetric key\<close>
 theorem Spy_not_see_encrypted_key:
-      "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
-                     Number cleartext, Nonce q, S2TTP|} \<in> set evs;
-         S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
+      "[|Says S R \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO, 
+                     Number cleartext, Nonce q, S2TTP\<rbrace> \<in> set evs;
+         S2TTP = Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>;
          evs \<in> certified_mail;
          S\<noteq>Spy; R \<notin> bad|]
       ==> Key K \<notin> analz(spies evs)"
@@ -430,10 +430,10 @@
 text\<open>Agent @{term R}, who may be the Spy, doesn't receive the key
  until @{term S} has access to the return receipt.\<close> 
 theorem S_guarantee:
-     "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
-                    Number cleartext, Nonce q, S2TTP|} \<in> set evs;
-        S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
-        Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs;
+     "[|Says S R \<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO, 
+                    Number cleartext, Nonce q, S2TTP\<rbrace> \<in> set evs;
+        S2TTP = Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>;
+        Notes R \<lbrace>Agent TTP, Agent R, Key K, hs\<rbrace> \<in> set evs;
         S\<noteq>Spy;  evs \<in> certified_mail|]
      ==> Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
 apply (erule rev_mp)
@@ -453,11 +453,11 @@
 theorem RR_validity:
   "[|Crypt (priSK TTP) S2TTP \<in> used evs;
      S2TTP = Crypt (pubEK TTP)
-               {|Agent S, Number AO, Key K, Agent R, 
-                 Hash {|Number cleartext, Nonce q, r, em|}|};
-     hr = Hash {|Number cleartext, Nonce q, r, em|};
+               \<lbrace>Agent S, Number AO, Key K, Agent R, 
+                 Hash \<lbrace>Number cleartext, Nonce q, r, em\<rbrace>\<rbrace>;
+     hr = Hash \<lbrace>Number cleartext, Nonce q, r, em\<rbrace>;
      R\<noteq>Spy;  evs \<in> certified_mail|]
-  ==> Notes R {|Agent TTP, Agent R, Key K, hr|} \<in> set evs"
+  ==> Notes R \<lbrace>Agent TTP, Agent R, Key K, hr\<rbrace> \<in> set evs"
 apply (erule rev_mp)
 apply (erule ssubst)
 apply (erule ssubst)
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Guard/Analz.thy
--- a/src/HOL/Auth/Guard/Analz.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Analz.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -17,8 +17,8 @@
   for H :: "msg set"
 where
   Inj [intro]: "[| X:H; is_MPair X |] ==> X:pparts H"
-| Fst [dest]: "[| {|X,Y|}:pparts H; is_MPair X |] ==> X:pparts H"
-| Snd [dest]: "[| {|X,Y|}:pparts H; is_MPair Y |] ==> Y:pparts H"
+| Fst [dest]: "[| \<lbrace>X,Y\<rbrace>:pparts H; is_MPair X |] ==> X:pparts H"
+| Snd [dest]: "[| \<lbrace>X,Y\<rbrace>:pparts H; is_MPair Y |] ==> Y:pparts H"
 
 subsection\<open>basic facts about @{term pparts}\<close>
 
@@ -53,8 +53,8 @@
 = pparts {X} Un pparts {Y} Un pparts H"
 by (rule eq, (erule pparts.induct, auto)+)
 
-lemma pparts_insert_MPair [iff]: "pparts (insert {|X,Y|} H)
-= insert {|X,Y|} (pparts ({X,Y} Un H))"
+lemma pparts_insert_MPair [iff]: "pparts (insert \<lbrace>X,Y\<rbrace> H)
+= insert \<lbrace>X,Y\<rbrace> (pparts ({X,Y} \<union> H))"
 apply (rule eq, (erule pparts.induct, auto)+)
 apply (rule_tac Y=Y in pparts.Fst, auto)
 apply (erule pparts.induct, auto)
@@ -119,8 +119,8 @@
   for H :: "msg set"
 where
   Inj [intro]: "[| X:H; not_MPair X |] ==> X:kparts H"
-| Fst [intro]: "[| {|X,Y|}:pparts H; not_MPair X |] ==> X:kparts H"
-| Snd [intro]: "[| {|X,Y|}:pparts H; not_MPair Y |] ==> Y:kparts H"
+| Fst [intro]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; not_MPair X |] ==> X:kparts H"
+| Snd [intro]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; not_MPair Y |] ==> Y:kparts H"
 
 subsection\<open>basic facts about @{term kparts}\<close>
 
@@ -137,8 +137,8 @@
 = kparts {X} Un kparts {Y} Un kparts H"
 by (rule eq, (erule kparts.induct, auto)+)
 
-lemma kparts_insert_MPair [iff]: "kparts (insert {|X,Y|} H)
-= kparts ({X,Y} Un H)"
+lemma kparts_insert_MPair [iff]: "kparts (insert \<lbrace>X,Y\<rbrace> H)
+= kparts ({X,Y} \<union> H)"
 by (rule eq, (erule kparts.induct, auto)+)
 
 lemma kparts_insert_Nonce [iff]: "kparts (insert (Nonce n) H)
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -51,11 +51,11 @@
 subsubsection\<open>messages that are pairs\<close>
 
 definition is_MPair :: "msg => bool" where
-"is_MPair X == EX Y Z. X = {|Y,Z|}"
+"is_MPair X == EX Y Z. X = \<lbrace>Y,Z\<rbrace>"
 
 declare is_MPair_def [simp]
 
-lemma MPair_is_MPair [iff]: "is_MPair {|X,Y|}"
+lemma MPair_is_MPair [iff]: "is_MPair \<lbrace>X,Y\<rbrace>"
 by simp
 
 lemma Agent_isnt_MPair [iff]: "~ is_MPair (Agent A)"
@@ -86,7 +86,7 @@
 declare is_MPair_def [simp del]
 
 definition has_no_pair :: "msg set => bool" where
-"has_no_pair H == ALL X Y. {|X,Y|} ~:H"
+"has_no_pair H == ALL X Y. \<lbrace>X,Y\<rbrace> \<notin> H"
 
 declare has_no_pair_def [simp]
 
@@ -218,7 +218,7 @@
 fun greatest_msg :: "msg => nat"
 where
   "greatest_msg (Nonce n) = n"
-| "greatest_msg {|X,Y|} = max (greatest_msg X) (greatest_msg Y)"
+| "greatest_msg \<lbrace>X,Y\<rbrace> = max (greatest_msg X) (greatest_msg Y)"
 | "greatest_msg (Crypt K X) = greatest_msg X"
 | "greatest_msg other = 0"
 
@@ -233,7 +233,7 @@
 lemma keyset_in [dest]: "[| keyset G; X:G |] ==> EX K. X = Key K"
 by (auto simp: keyset_def)
 
-lemma MPair_notin_keyset [simp]: "keyset G ==> {|X,Y|} ~:G"
+lemma MPair_notin_keyset [simp]: "keyset G ==> \<lbrace>X,Y\<rbrace> \<notin> G"
 by auto
 
 lemma Crypt_notin_keyset [simp]: "keyset G ==> Crypt K X ~:G"
@@ -332,7 +332,7 @@
 
 subsubsection\<open>lemma on knows\<close>
 
-lemma Says_imp_spies2: "Says A B {|X,Y|}:set evs ==> Y:parts (spies evs)"
+lemma Says_imp_spies2: "Says A B \<lbrace>X,Y\<rbrace> \<in> set evs ==> Y \<in> parts (spies evs)"
 by (drule Says_imp_spies, drule parts.Inj, drule parts.Snd, simp)
 
 lemma Says_not_parts: "[| Says A B X:set evs; Y ~:parts (spies evs) |]
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Guard/Guard.thy
--- a/src/HOL/Auth/Guard/Guard.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -19,7 +19,7 @@
   No_Nonce [intro]: "Nonce n ~:parts {X} ==> X:guard n Ks"
 | Guard_Nonce [intro]: "invKey K:Ks ==> Crypt K X:guard n Ks"
 | Crypt [intro]: "X:guard n Ks ==> Crypt K X:guard n Ks"
-| Pair [intro]: "[| X:guard n Ks; Y:guard n Ks |] ==> {|X,Y|}:guard n Ks"
+| Pair [intro]: "[| X:guard n Ks; Y:guard n Ks |] ==> \<lbrace>X,Y\<rbrace> \<in> guard n Ks"
 
 subsection\<open>basic facts about @{term guard}\<close>
 
@@ -58,8 +58,8 @@
 lemma guard_Crypt: "[| Crypt K Y:guard n Ks; K ~:invKey`Ks |] ==> Y:guard n Ks"
   by (ind_cases "Crypt K Y:guard n Ks") (auto intro!: image_eqI)
 
-lemma guard_MPair [iff]: "({|X,Y|}:guard n Ks) = (X:guard n Ks & Y:guard n Ks)"
-by (auto, (ind_cases "{|X,Y|}:guard n Ks", auto)+)
+lemma guard_MPair [iff]: "(\<lbrace>X,Y\<rbrace> \<in> guard n Ks) = (X \<in> guard n Ks \<and> Y \<in> guard n Ks)"
+by (auto, (ind_cases "\<lbrace>X,Y\<rbrace> \<in> guard n Ks", auto)+)
 
 lemma guard_not_guard [rule_format]: "X:guard n Ks ==>
 Crypt K Y:kparts {X} --> Nonce n:kparts {Y} --> Y ~:guard n Ks"
@@ -175,7 +175,7 @@
 fun crypt_nb :: "msg => nat"
 where
   "crypt_nb (Crypt K X) = Suc (crypt_nb X)"
-| "crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y"
+| "crypt_nb \<lbrace>X,Y\<rbrace> = crypt_nb X + crypt_nb Y"
 | "crypt_nb X = 0" (* otherwise *)
 
 subsection\<open>basic facts about @{term crypt_nb}\<close>
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Guard/GuardK.thy
--- a/src/HOL/Auth/Guard/GuardK.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -26,7 +26,7 @@
   No_Key [intro]: "Key n ~:parts {X} ==> X:guardK n Ks"
 | Guard_Key [intro]: "invKey K:Ks ==> Crypt K X:guardK n Ks"
 | Crypt [intro]: "X:guardK n Ks ==> Crypt K X:guardK n Ks"
-| Pair [intro]: "[| X:guardK n Ks; Y:guardK n Ks |] ==> {|X,Y|}:guardK n Ks"
+| Pair [intro]: "[| X:guardK n Ks; Y:guardK n Ks |] ==> \<lbrace>X,Y\<rbrace>:guardK n Ks"
 
 subsection\<open>basic facts about @{term guardK}\<close>
 
@@ -65,9 +65,9 @@
 lemma guardK_Crypt: "[| Crypt K Y:guardK n Ks; K ~:invKey`Ks |] ==> Y:guardK n Ks"
   by (ind_cases "Crypt K Y:guardK n Ks") (auto intro!: image_eqI)
 
-lemma guardK_MPair [iff]: "({|X,Y|}:guardK n Ks)
+lemma guardK_MPair [iff]: "(\<lbrace>X,Y\<rbrace>:guardK n Ks)
 = (X:guardK n Ks & Y:guardK n Ks)"
-by (auto, (ind_cases "{|X,Y|}:guardK n Ks", auto)+)
+by (auto, (ind_cases "\<lbrace>X,Y\<rbrace>:guardK n Ks", auto)+)
 
 lemma guardK_not_guardK [rule_format]: "X:guardK n Ks ==>
 Crypt K Y:kparts {X} --> Key n:kparts {Y} --> Y ~:guardK n Ks"
@@ -172,7 +172,7 @@
 
 fun crypt_nb :: "msg => nat" where
 "crypt_nb (Crypt K X) = Suc (crypt_nb X)" |
-"crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y" |
+"crypt_nb \<lbrace>X,Y\<rbrace> = crypt_nb X + crypt_nb Y" |
 "crypt_nb X = 0" (* otherwise *)
 
 subsection\<open>basic facts about @{term crypt_nb}\<close>
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Guard/Guard_NS_Public.thy
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -13,19 +13,19 @@
 
 abbreviation (input)
   ns1 :: "agent => agent => nat => event" where
-  "ns1 A B NA == Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
+  "ns1 A B NA == Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"
 
 abbreviation (input)
   ns1' :: "agent => agent => agent => nat => event" where
-  "ns1' A' A B NA == Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
+  "ns1' A' A B NA == Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"
 
 abbreviation (input)
   ns2 :: "agent => agent => nat => nat => event" where
-  "ns2 B A NA NB == Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
+  "ns2 B A NA NB == Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"
 
 abbreviation (input)
   ns2' :: "agent => agent => agent => nat => nat => event" where
-  "ns2' B' B A NA NB == Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
+  "ns2' B' B A NA NB == Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"
 
 abbreviation (input)
   ns3 :: "agent => agent => nat => event" where
@@ -80,28 +80,28 @@
 subsection\<open>nonce are used only once\<close>
 
 lemma NA_is_uniq [rule_format]: "evs:nsp ==>
-Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
---> Crypt (pubK B') {|Nonce NA, Agent A'|}:parts (spies evs)
+Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>:parts (spies evs)
+--> Crypt (pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace>:parts (spies evs)
 --> Nonce NA ~:analz (spies evs) --> A=A' & B=B'"
 apply (erule nsp.induct, simp_all)
 by (blast intro: analz_insertI)+
 
 lemma no_Nonce_NS1_NS2 [rule_format]: "evs:nsp ==>
-Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs)
---> Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
+Crypt (pubK B') \<lbrace>Nonce NA', Nonce NA, Agent A'\<rbrace>:parts (spies evs)
+--> Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>:parts (spies evs)
 --> Nonce NA:analz (spies evs)"
 apply (erule nsp.induct, simp_all)
 by (blast intro: analz_insertI)+
 
 lemma no_Nonce_NS1_NS2' [rule_format]:
-"[| Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs);
-Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs); evs:nsp |]
+"[| Crypt (pubK B') \<lbrace>Nonce NA', Nonce NA, Agent A'\<rbrace>:parts (spies evs);
+Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>:parts (spies evs); evs:nsp |]
 ==> Nonce NA:analz (spies evs)"
 by (rule no_Nonce_NS1_NS2, auto)
  
 lemma NB_is_uniq [rule_format]: "evs:nsp ==>
-Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
---> Crypt (pubK A') {|Nonce NA', Nonce NB, Agent B'|}:parts (spies evs)
+Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>:parts (spies evs)
+--> Crypt (pubK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace>:parts (spies evs)
 --> Nonce NB ~:analz (spies evs) --> A=A' & B=B' & NA=NA'"
 apply (erule nsp.induct, simp_all)
 by (blast intro: analz_insertI)+
@@ -166,13 +166,13 @@
 subsection\<open>Agents' Authentication\<close>
 
 lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
-Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
+Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>:parts (spies evs)
 --> Nonce NA ~:analz (spies evs) --> ns1 A B NA:set evs"
 apply (erule nsp.induct, simp_all)
 by (blast intro: analz_insertI)+
 
 lemma A_trusts_NS2: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns1 A B NA:set evs
---> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
+--> Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>:parts (spies evs)
 --> ns2 B A NA NB:set evs"
 apply (erule nsp.induct, simp_all, safe)
 apply (frule_tac B=B in ns1_imp_Guard, simp+)
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Guard/Guard_OtwayRees.thy
--- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -16,43 +16,43 @@
 abbreviation
   or1 :: "agent => agent => nat => event" where
   "or1 A B NA ==
-    Says A B {|Nonce NA, Agent A, Agent B, Ciph A {|Nonce NA, Agent A, Agent B|}|}"
+    Says A B \<lbrace>Nonce NA, Agent A, Agent B, Ciph A \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace>"
 
 abbreviation
   or1' :: "agent => agent => agent => nat => msg => event" where
-  "or1' A' A B NA X == Says A' B {|Nonce NA, Agent A, Agent B, X|}"
+  "or1' A' A B NA X == Says A' B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace>"
 
 abbreviation
   or2 :: "agent => agent => nat => nat => msg => event" where
   "or2 A B NA NB X ==
-    Says B Server {|Nonce NA, Agent A, Agent B, X,
-                    Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
+    Says B Server \<lbrace>Nonce NA, Agent A, Agent B, X,
+                    Ciph B \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>"
 
 abbreviation
   or2' :: "agent => agent => agent => nat => nat => event" where
   "or2' B' A B NA NB ==
-    Says B' Server {|Nonce NA, Agent A, Agent B,
-                     Ciph A {|Nonce NA, Agent A, Agent B|},
-                     Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
+    Says B' Server \<lbrace>Nonce NA, Agent A, Agent B,
+                     Ciph A \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>,
+                     Ciph B \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>"
 
 abbreviation
   or3 :: "agent => agent => nat => nat => key => event" where
   "or3 A B NA NB K ==
-    Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
-                    Ciph B {|Nonce NB, Key K|}|}"
+    Says Server B \<lbrace>Nonce NA, Ciph A \<lbrace>Nonce NA, Key K\<rbrace>,
+                    Ciph B \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>"
 
 abbreviation
   or3':: "agent => msg => agent => agent => nat => nat => key => event" where
   "or3' S Y A B NA NB K ==
-    Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
+    Says S B \<lbrace>Nonce NA, Y, Ciph B \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>"
 
 abbreviation
   or4 :: "agent => agent => nat => msg => event" where
-  "or4 A B NA X == Says B A {|Nonce NA, X, nil|}"
+  "or4 A B NA X == Says B A \<lbrace>Nonce NA, X, nil\<rbrace>"
 
 abbreviation
   or4' :: "agent => agent => nat => key => event" where
-  "or4' B' A NA K == Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
+  "or4' B' A NA K == Says B' A \<lbrace>Nonce NA, Ciph A \<lbrace>Nonce NA, Key K\<rbrace>, nil\<rbrace>"
 
 subsection\<open>definition of the protocol\<close>
 
@@ -108,7 +108,7 @@
 ==> X:parts (spies evs)"
 by blast
 
-lemma or3_parts_spies [dest]: "Says S B {|NA, Y, Ciph B {|NB, K|}|}:set evs
+lemma or3_parts_spies [dest]: "Says S B \<lbrace>NA, Y, Ciph B \<lbrace>NB, K\<rbrace>\<rbrace>:set evs
 ==> K:parts (spies evs)"
 by blast
 
@@ -169,13 +169,13 @@
 apply (case_tac "Aa=B", clarsimp)
 apply (case_tac "NAa=NB", clarsimp)
 apply (drule Says_imp_spies)
-apply (drule_tac Y="{|Nonce NB, Agent Aa, Agent Ba|}"
+apply (drule_tac Y="\<lbrace>Nonce NB, Agent Aa, Agent Ba\<rbrace>"
                  and K="shrK Aa" in in_Guard_kparts_Crypt, simp+)
 apply (simp add: No_Nonce) 
 apply (case_tac "Ba=B", clarsimp)
 apply (case_tac "NBa=NB", clarify)
 apply (drule Says_imp_spies)
-apply (drule_tac Y="{|Nonce NAa, Nonce NB, Agent Aa, Agent Ba|}"
+apply (drule_tac Y="\<lbrace>Nonce NAa, Nonce NB, Agent Aa, Agent Ba\<rbrace>"
                  and K="shrK Ba" in in_Guard_kparts_Crypt, simp+)
 apply (simp add: No_Nonce) 
 (* OR4 *)
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Guard/Guard_Public.thy
--- a/src/HOL/Auth/Guard/Guard_Public.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Guard_Public.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -14,7 +14,7 @@
 subsubsection\<open>signature\<close>
 
 definition sign :: "agent => msg => msg" where
-"sign A X == {|Agent A, X, Crypt (priK A) (Hash X)|}"
+"sign A X == \<lbrace>Agent A, X, Crypt (priK A) (Hash X)\<rbrace>"
 
 lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')"
 by (auto simp: sign_def)
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Guard/Guard_Yahalom.thy
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -11,38 +11,38 @@
 
 abbreviation (input)
   ya1 :: "agent => agent => nat => event" where
-  "ya1 A B NA == Says A B {|Agent A, Nonce NA|}"
+  "ya1 A B NA == Says A B \<lbrace>Agent A, Nonce NA\<rbrace>"
 
 abbreviation (input)
   ya1' :: "agent => agent => agent => nat => event" where
-  "ya1' A' A B NA == Says A' B {|Agent A, Nonce NA|}"
+  "ya1' A' A B NA == Says A' B \<lbrace>Agent A, Nonce NA\<rbrace>"
 
 abbreviation (input)
   ya2 :: "agent => agent => nat => nat => event" where
-  "ya2 A B NA NB == Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
+  "ya2 A B NA NB == Says B Server \<lbrace>Agent B, Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>"
 
 abbreviation (input)
   ya2' :: "agent => agent => agent => nat => nat => event" where
-  "ya2' B' A B NA NB == Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
+  "ya2' B' A B NA NB == Says B' Server \<lbrace>Agent B, Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>"
 
 abbreviation (input)
   ya3 :: "agent => agent => nat => nat => key => event" where
   "ya3 A B NA NB K ==
-    Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
-                    Ciph B {|Agent A, Key K|}|}"
+    Says Server A \<lbrace>Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>,
+                    Ciph B \<lbrace>Agent A, Key K\<rbrace>\<rbrace>"
 
 abbreviation (input)
   ya3':: "agent => msg => agent => agent => nat => nat => key => event" where
   "ya3' S Y A B NA NB K ==
-    Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
+    Says S A \<lbrace>Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, Y\<rbrace>"
 
 abbreviation (input)
   ya4 :: "agent => agent => nat => nat => msg => event" where
-  "ya4 A B K NB Y == Says A B {|Y, Crypt K (Nonce NB)|}"
+  "ya4 A B K NB Y == Says A B \<lbrace>Y, Crypt K (Nonce NB)\<rbrace>"
 
 abbreviation (input)
   ya4' :: "agent => agent => nat => nat => msg => event" where
-  "ya4' A' B K NB Y == Says A' B {|Y, Crypt K (Nonce NB)|}"
+  "ya4' A' B K NB Y == Says A' B \<lbrace>Y, Crypt K (Nonce NB)\<rbrace>"
 
 
 subsection\<open>definition of the protocol\<close>
@@ -128,19 +128,19 @@
 
 lemma ya2'_parts_imp_ya1'_parts [rule_format]:
      "[| evs:ya; B ~:bad |] ==>
-      Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
-      {|Agent A, Nonce NA|}:spies evs"
+      Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>:parts (spies evs) -->
+      \<lbrace>Agent A, Nonce NA\<rbrace>:spies evs"
 by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts)
 
 lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB:set evs; evs:ya; B ~:bad |]
-==> {|Agent A, Nonce NA|}:spies evs"
+==> \<lbrace>Agent A, Nonce NA\<rbrace>:spies evs"
 by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts)
 
 subsection\<open>uniqueness of NB\<close>
 
 lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs:ya; B ~:bad; B' ~:bad |] ==>
-Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
-Ciph B' {|Agent A', Nonce NA', Nonce NB|}:parts (spies evs) -->
+Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>:parts (spies evs) -->
+Ciph B' \<lbrace>Agent A', Nonce NA', Nonce NB\<rbrace>:parts (spies evs) -->
 A=A' & B=B' & NA=NA'"
 apply (erule ya.induct, simp_all, clarify)
 apply (drule Crypt_synth_insert, simp+)
@@ -156,15 +156,15 @@
 subsection\<open>ya3' implies ya2'\<close>
 
 lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs:ya; A ~:bad |] ==>
-Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
---> Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs)"
+Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>:parts (spies evs)
+--> Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>:parts (spies evs)"
 apply (erule ya.induct, simp_all)
 apply (clarify, drule Crypt_synth_insert, simp+)
 apply (blast intro: parts_sub, blast)
 by (auto dest: Says_imp_spies parts_parts)
 
 lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs:ya; A ~:bad |] ==>
-Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
+Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>:parts (spies evs)
 --> (EX B'. ya2' B' A B NA NB:set evs)"
 apply (erule ya.induct, simp_all, safe)
 apply (drule Crypt_synth_insert, simp+)
@@ -180,7 +180,7 @@
 subsection\<open>ya3' implies ya3\<close>
 
 lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs:ya; A ~:bad |] ==>
-Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts(spies evs)
+Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>:parts(spies evs)
 --> ya3 A B NA NB K:set evs"
 apply (erule ya.induct, simp_all, safe)
 apply (drule Crypt_synth_insert, simp+)
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Guard/List_Msg.thy
--- a/src/HOL/Auth/Guard/List_Msg.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/List_Msg.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -13,7 +13,7 @@
 
 abbreviation (input)
   cons :: "msg => msg => msg" where
-  "cons x l == {|x,l|}"
+  "cons x l == \<lbrace>x,l\<rbrace>"
 
 subsubsection\<open>induction principle\<close>
 
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Guard/P1.thy
--- a/src/HOL/Auth/Guard/P1.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/P1.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -18,7 +18,7 @@
 the contents of the messages are not completely specified in the paper
 we assume that the user sends his request and his itinerary in the clear
 
-we will adopt the following format for messages: {|A,r,I,L|}
+we will adopt the following format for messages: \<lbrace>A,r,I,L\<rbrace>
 A: originator (agent)
 r: request (number)
 I: next shops (agent list)
@@ -36,8 +36,8 @@
 definition chain :: "agent => nat => agent => msg => agent => msg" where
 "chain B ofr A L C ==
 let m1= Crypt (pubK A) (Nonce ofr) in
-let m2= Hash {|head L, Agent C|} in
-sign B {|m1,m2|}"
+let m2= Hash \<lbrace>head L, Agent C\<rbrace> in
+sign B \<lbrace>m1,m2\<rbrace>"
 
 declare Let_def [simp]
 
@@ -51,7 +51,7 @@
 subsubsection\<open>agent whose key is used to sign an offer\<close>
 
 fun shop :: "msg => msg" where
-"shop {|B,X,Crypt K H|} = Agent (agt K)"
+"shop \<lbrace>B,X,Crypt K H\<rbrace> = Agent (agt K)"
 
 lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B"
 by (simp add: chain_def sign_def)
@@ -59,7 +59,7 @@
 subsubsection\<open>nonce used in an offer\<close>
 
 fun nonce :: "msg => msg" where
-"nonce {|B,{|Crypt K ofr,m2|},CryptH|} = ofr"
+"nonce \<lbrace>B,\<lbrace>Crypt K ofr,m2\<rbrace>,CryptH\<rbrace> = ofr"
 
 lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr"
 by (simp add: chain_def sign_def)
@@ -67,7 +67,7 @@
 subsubsection\<open>next shop\<close>
 
 fun next_shop :: "msg => agent" where
-"next_shop {|B,{|m1,Hash{|headL,Agent C|}|},CryptH|} = C"
+"next_shop \<lbrace>B,\<lbrace>m1,Hash\<lbrace>headL,Agent C\<rbrace>\<rbrace>,CryptH\<rbrace> = C"
 
 lemma next_shop_chain [iff]: "next_shop (chain B ofr A L C) = C"
 by (simp add: chain_def sign_def)
@@ -96,8 +96,8 @@
 subsubsection\<open>request event\<close>
 
 definition reqm :: "agent => nat => nat => msg => agent => msg" where
-"reqm A r n I B == {|Agent A, Number r, cons (Agent A) (cons (Agent B) I),
-cons (anchor A n B) nil|}"
+"reqm A r n I B == \<lbrace>Agent A, Number r, cons (Agent A) (cons (Agent B) I),
+cons (anchor A n B) nil\<rbrace>"
 
 lemma reqm_inj [iff]: "(reqm A r n I B = reqm A' r' n' I' B')
 = (A=A' & r=r' & n=n' & I=I' & B=B')"
@@ -117,8 +117,8 @@
 
 definition prom :: "agent => nat => agent => nat => msg => msg =>
 msg => agent => msg" where
-"prom B ofr A r I L J C == {|Agent A, Number r,
-app (J, del (Agent B, I)), cons (chain B ofr A L C) L|}"
+"prom B ofr A r I L J C == \<lbrace>Agent A, Number r,
+app (J, del (Agent B, I)), cons (chain B ofr A L C) L\<rbrace>"
 
 lemma prom_inj [dest]: "prom B ofr A r I L J C
 = prom B' ofr' A' r' I' L' J' C'
@@ -147,7 +147,7 @@
 
 | Request: "[| evsr:p1; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p1"
 
-| Propose: "[| evsp:p1; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp;
+| Propose: "[| evsp:p1; Says A' B \<lbrace>Agent A,Number r,I,cons M L\<rbrace>:set evsp;
   I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I)));
   Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p1"
 
@@ -198,7 +198,7 @@
 subsubsection\<open>list of offers\<close>
 
 fun offers :: "msg => msg" where
-"offers (cons M L) = cons {|shop M, nonce M|} (offers L)" |
+"offers (cons M L) = cons \<lbrace>shop M, nonce M\<rbrace> (offers L)" |
 "offers other = nil"
 
 subsubsection\<open>list of agents whose keys are used to sign a list of offers\<close>
@@ -262,15 +262,15 @@
 apply clarify
 apply (frule len_not_empty, clarsimp)
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,xa,l'a|}:valid A n B" for x xa l'a)
-apply (ind_cases "{|x,M,l'a|}:valid A n B" for x l'a)
+apply (ind_cases "\<lbrace>x,xa,l'a\<rbrace>:valid A n B" for x xa l'a)
+apply (ind_cases "\<lbrace>x,M,l'a\<rbrace>:valid A n B" for x l'a)
 apply (simp add: chain_def)
 (* i > 0 *)
 apply clarify
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na)
+apply (ind_cases "\<lbrace>x,repl(l',Suc na,M)\<rbrace>:valid A n B" for x l' na)
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
 by (drule_tac x=l' in spec, simp, blast)
 
 subsubsection\<open>insertion resilience:
@@ -286,15 +286,15 @@
 (* i = 0 *)
 apply clarify
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l', simp)
-apply (ind_cases "{|x,M,l'|}:valid A n B" for x l', clarsimp)
-apply (ind_cases "{|head l',l'|}:valid A n B" for l', simp, simp)
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l', simp)
+apply (ind_cases "\<lbrace>x,M,l'\<rbrace>:valid A n B" for x l', clarsimp)
+apply (ind_cases "\<lbrace>head l',l'\<rbrace>:valid A n B" for l', simp, simp)
 (* i > 0 *)
 apply clarify
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na)
+apply (ind_cases "\<lbrace>x,ins(l',Suc na,M)\<rbrace>:valid A n B" for x l' na)
 apply (frule len_not_empty, clarsimp)
 by (drule_tac x=l' in spec, clarsimp)
 
@@ -307,14 +307,14 @@
 (* i = 0 *)
 apply clarify
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|M,l'|}:valid A n B" for l')
+apply (ind_cases "\<lbrace>M,l'\<rbrace>:valid A n B" for l')
 apply (frule len_not_empty, clarsimp, simp)
 (* i > 0 *)
 apply clarify
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
 apply (frule len_not_empty, clarsimp)
 by (drule_tac x=l' in spec, clarsimp)
 
@@ -326,7 +326,7 @@
 
 subsubsection\<open>get components of a message\<close>
 
-lemma get_ML [dest]: "Says A' B {|A,r,I,M,L|}:set evs ==>
+lemma get_ML [dest]: "Says A' B \<lbrace>A,r,I,M,L\<rbrace>:set evs ==>
 M:parts (spies evs) & L:parts (spies evs)"
 by blast
 
@@ -400,15 +400,15 @@
 lemma agl_guard [intro]: "I:agl ==> I:guard n Ks"
 by (erule agl.induct, auto)
 
-lemma Says_to_knows_max'_guard: "[| Says A' C {|A'',r,I,L|}:set evs;
+lemma Says_to_knows_max'_guard: "[| Says A' C \<lbrace>A'',r,I,L\<rbrace>:set evs;
 Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
 by (auto dest: Says_to_knows_max')
 
-lemma Says_from_knows_max'_guard: "[| Says C A' {|A'',r,I,L|}:set evs;
+lemma Says_from_knows_max'_guard: "[| Says C A' \<lbrace>A'',r,I,L\<rbrace>:set evs;
 Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
 by (auto dest: Says_from_knows_max')
 
-lemma Says_Nonce_not_used_guard: "[| Says A' B {|A'',r,I,L|}:set evs;
+lemma Says_Nonce_not_used_guard: "[| Says A' B \<lbrace>A'',r,I,L\<rbrace>:set evs;
 Nonce n ~:used evs |] ==> L:guard n Ks"
 by (drule not_used_not_parts, auto)
 
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Guard/P2.thy
--- a/src/HOL/Auth/Guard/P2.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/P2.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -23,8 +23,8 @@
 definition chain :: "agent => nat => agent => msg => agent => msg" where
 "chain B ofr A L C ==
 let m1= sign B (Nonce ofr) in
-let m2= Hash {|head L, Agent C|} in
-{|Crypt (pubK A) m1, m2|}"
+let m2= Hash \<lbrace>head L, Agent C\<rbrace> in
+\<lbrace>Crypt (pubK A) m1, m2\<rbrace>"
 
 declare Let_def [simp]
 
@@ -38,7 +38,7 @@
 subsubsection\<open>agent whose key is used to sign an offer\<close>
 
 fun shop :: "msg => msg" where
-"shop {|Crypt K {|B,ofr,Crypt K' H|},m2|} = Agent (agt K')"
+"shop \<lbrace>Crypt K \<lbrace>B,ofr,Crypt K' H\<rbrace>,m2\<rbrace> = Agent (agt K')"
 
 lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B"
 by (simp add: chain_def sign_def)
@@ -46,7 +46,7 @@
 subsubsection\<open>nonce used in an offer\<close>
 
 fun nonce :: "msg => msg" where
-"nonce {|Crypt K {|B,ofr,CryptH|},m2|} = ofr"
+"nonce \<lbrace>Crypt K \<lbrace>B,ofr,CryptH\<rbrace>,m2\<rbrace> = ofr"
 
 lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr"
 by (simp add: chain_def sign_def)
@@ -54,7 +54,7 @@
 subsubsection\<open>next shop\<close>
 
 fun next_shop :: "msg => agent" where
-"next_shop {|m1,Hash {|headL,Agent C|}|} = C"
+"next_shop \<lbrace>m1,Hash \<lbrace>headL,Agent C\<rbrace>\<rbrace> = C"
 
 lemma "next_shop (chain B ofr A L C) = C"
 by (simp add: chain_def sign_def)
@@ -77,8 +77,8 @@
 subsubsection\<open>request event\<close>
 
 definition reqm :: "agent => nat => nat => msg => agent => msg" where
-"reqm A r n I B == {|Agent A, Number r, cons (Agent A) (cons (Agent B) I),
-cons (anchor A n B) nil|}"
+"reqm A r n I B == \<lbrace>Agent A, Number r, cons (Agent A) (cons (Agent B) I),
+cons (anchor A n B) nil\<rbrace>"
 
 lemma reqm_inj [iff]: "(reqm A r n I B = reqm A' r' n' I' B')
 = (A=A' & r=r' & n=n' & I=I' & B=B')"
@@ -98,8 +98,8 @@
 
 definition prom :: "agent => nat => agent => nat => msg => msg =>
 msg => agent => msg" where
-"prom B ofr A r I L J C == {|Agent A, Number r,
-app (J, del (Agent B, I)), cons (chain B ofr A L C) L|}"
+"prom B ofr A r I L J C == \<lbrace>Agent A, Number r,
+app (J, del (Agent B, I)), cons (chain B ofr A L C) L\<rbrace>"
 
 lemma prom_inj [dest]: "prom B ofr A r I L J C = prom B' ofr' A' r' I' L' J' C'
 ==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'"
@@ -127,7 +127,7 @@
 
 | Request: "[| evsr:p2; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p2"
 
-| Propose: "[| evsp:p2; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp;
+| Propose: "[| evsp:p2; Says A' B \<lbrace>Agent A,Number r,I,cons M L\<rbrace>:set evsp;
   I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I)));
   Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p2"
 
@@ -154,7 +154,7 @@
 
 fun offers :: "msg => msg"
 where
-  "offers (cons M L) = cons {|shop M, nonce M|} (offers L)"
+  "offers (cons M L) = cons \<lbrace>shop M, nonce M\<rbrace> (offers L)"
 | "offers other = nil"
 
 
@@ -173,15 +173,15 @@
 apply clarify
 apply (frule len_not_empty, clarsimp)
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,xa,l'a|}:valid A n B" for x xa l'a)
-apply (ind_cases "{|x,M,l'a|}:valid A n B" for x l'a)
+apply (ind_cases "\<lbrace>x,xa,l'a\<rbrace>:valid A n B" for x xa l'a)
+apply (ind_cases "\<lbrace>x,M,l'a\<rbrace>:valid A n B" for x l'a)
 apply (simp add: chain_def)
 (* i > 0 *)
 apply clarify
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na)
+apply (ind_cases "\<lbrace>x,repl(l',Suc na,M)\<rbrace>:valid A n B" for x l' na)
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
 by (drule_tac x=l' in spec, simp, blast)
 
 subsection\<open>insertion resilience:
@@ -197,15 +197,15 @@
 (* i = 0 *)
 apply clarify
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l', simp)
-apply (ind_cases "{|x,M,l'|}:valid A n B" for x l', clarsimp)
-apply (ind_cases "{|head l',l'|}:valid A n B" for l', simp, simp)
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l', simp)
+apply (ind_cases "\<lbrace>x,M,l'\<rbrace>:valid A n B" for x l', clarsimp)
+apply (ind_cases "\<lbrace>head l',l'\<rbrace>:valid A n B" for l', simp, simp)
 (* i > 0 *)
 apply clarify
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na)
+apply (ind_cases "\<lbrace>x,ins(l',Suc na,M)\<rbrace>:valid A n B" for x l' na)
 apply (frule len_not_empty, clarsimp)
 by (drule_tac x=l' in spec, clarsimp)
 
@@ -218,14 +218,14 @@
 (* i = 0 *)
 apply clarify
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|M,l'|}:valid A n B" for l')
+apply (ind_cases "\<lbrace>M,l'\<rbrace>:valid A n B" for l')
 apply (frule len_not_empty, clarsimp, simp)
 (* i > 0 *)
 apply clarify
 apply (frule len_not_empty, clarsimp)
-apply (ind_cases "{|x,l'|}:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
 apply (frule len_not_empty, clarsimp)
 by (drule_tac x=l' in spec, clarsimp)
 
@@ -237,7 +237,7 @@
 
 subsection\<open>get components of a message\<close>
 
-lemma get_ML [dest]: "Says A' B {|A,R,I,M,L|}:set evs ==>
+lemma get_ML [dest]: "Says A' B \<lbrace>A,R,I,M,L\<rbrace>:set evs ==>
 M:parts (spies evs) & L:parts (spies evs)"
 by blast
 
@@ -312,15 +312,15 @@
 lemma agl_guard [intro]: "I:agl ==> I:guard n Ks"
 by (erule agl.induct, auto)
 
-lemma Says_to_knows_max'_guard: "[| Says A' C {|A'',r,I,L|}:set evs;
+lemma Says_to_knows_max'_guard: "[| Says A' C \<lbrace>A'',r,I,L\<rbrace>:set evs;
 Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
 by (auto dest: Says_to_knows_max')
 
-lemma Says_from_knows_max'_guard: "[| Says C A' {|A'',r,I,L|}:set evs;
+lemma Says_from_knows_max'_guard: "[| Says C A' \<lbrace>A'',r,I,L\<rbrace>:set evs;
 Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
 by (auto dest: Says_from_knows_max')
 
-lemma Says_Nonce_not_used_guard: "[| Says A' B {|A'',r,I,L|}:set evs;
+lemma Says_Nonce_not_used_guard: "[| Says A' B \<lbrace>A'',r,I,L\<rbrace>:set evs;
 Nonce n ~:used evs |] ==> L:guard n Ks"
 by (drule not_used_not_parts, auto)
 
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Guard/Proto.thy
--- a/src/HOL/Auth/Guard/Proto.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -39,7 +39,7 @@
 if (EX A. K = pubK A) then Crypt (pubK (agent s (agt K))) (apm s X)
 else if (EX A. K = priK A) then Crypt (priK (agent s (agt K))) (apm s X)
 else Crypt (key s K) (apm s X))"
-| "apm s {|X,Y|} = {|apm s X, apm s Y|}"
+| "apm s \<lbrace>X,Y\<rbrace> = \<lbrace>apm s X, apm s Y\<rbrace>"
 
 lemma apm_parts: "X:parts {Y} ==> apm s X:parts {apm s Y}"
 apply (erule parts.induct, simp_all, blast)
@@ -371,17 +371,17 @@
 
 abbreviation
   ns1 :: rule where
-  "ns1 == ({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
+  "ns1 == ({}, Says a b (Crypt (pubK b) \<lbrace>Nonce Na, Agent a\<rbrace>))"
 
 abbreviation
   ns2 :: rule where
-  "ns2 == ({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})},
-    Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))"
+  "ns2 == ({Says a' b (Crypt (pubK b) \<lbrace>Nonce Na, Agent a\<rbrace>)},
+    Says b a (Crypt (pubK a) \<lbrace>Nonce Na, Nonce Nb, Agent b\<rbrace>))"
 
 abbreviation
   ns3 :: rule where
-  "ns3 == ({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}),
-    Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})},
+  "ns3 == ({Says a b (Crypt (pubK b) \<lbrace>Nonce Na, Agent a\<rbrace>),
+    Says b' a (Crypt (pubK a) \<lbrace>Nonce Na, Nonce Nb, Agent b\<rbrace>)},
     Says a b (Crypt (pubK b) (Nonce Nb)))"
 
 inductive_set ns :: proto where
@@ -391,11 +391,11 @@
 
 abbreviation (input)
   ns3a :: event where
-  "ns3a == Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
+  "ns3a == Says a b (Crypt (pubK b) \<lbrace>Nonce Na, Agent a\<rbrace>)"
 
 abbreviation (input)
   ns3b :: event where
-  "ns3b == Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})"
+  "ns3b == Says b' a (Crypt (pubK a) \<lbrace>Nonce Na, Nonce Nb, Agent b\<rbrace>)"
 
 definition keys :: "keyfun" where
 "keys R' s' n evs == {priK' s' a, priK' s' b}"
@@ -405,8 +405,8 @@
 
 definition secret :: "secfun" where
 "secret R n s Ks ==
-(if R=ns1 then apm s (Crypt (pubK b) {|Nonce Na, Agent a|})
-else if R=ns2 then apm s (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})
+(if R=ns1 then apm s (Crypt (pubK b) \<lbrace>Nonce Na, Agent a\<rbrace>)
+else if R=ns2 then apm s (Crypt (pubK a) \<lbrace>Nonce Na, Nonce Nb, Agent b\<rbrace>)
 else Number 0)"
 
 definition inf :: "rule => rule => bool" where
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Message.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -48,21 +48,17 @@
          | Crypt  key msg   \<comment>\<open>Encryption, public- or shared-key\<close>
 
 
-text\<open>Concrete syntax: messages appear as {|A,B,NA|}, etc...\<close>
+text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
 syntax
-  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
-
-syntax (xsymbols)
-  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
-
+  "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
 translations
-  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
-  "{|x, y|}"      == "CONST MPair x y"
+  "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+  "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
 
 
 definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
     \<comment>\<open>Message Y paired with a MAC computed with the help of X\<close>
-    "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
+    "Hash[X] Y == \<lbrace>Hash\<lbrace>X,Y\<rbrace>, Y\<rbrace>"
 
 definition keysFor :: "msg set => key set" where
     \<comment>\<open>Keys useful to decrypt elements of a message set\<close>
@@ -75,9 +71,9 @@
   parts :: "msg set => msg set"
   for H :: "msg set"
   where
-    Inj [intro]:               "X \<in> H ==> X \<in> parts H"
-  | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
-  | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
+    Inj [intro]: "X \<in> H ==> X \<in> parts H"
+  | Fst:         "\<lbrace>X,Y\<rbrace> \<in> parts H ==> X \<in> parts H"
+  | Snd:         "\<lbrace>X,Y\<rbrace> \<in> parts H ==> Y \<in> parts H"
   | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
 
 
@@ -136,7 +132,7 @@
 lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
-lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
+lemma keysFor_insert_MPair [simp]: "keysFor (insert \<lbrace>X,Y\<rbrace> H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Crypt [simp]: 
@@ -153,7 +149,7 @@
 subsection\<open>Inductive relation "parts"\<close>
 
 lemma MPair_parts:
-     "[| {|X,Y|} \<in> parts H;        
+     "[| \<lbrace>X,Y\<rbrace> \<in> parts H;        
          [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
 by (blast dest: parts.Fst parts.Snd) 
 
@@ -294,8 +290,8 @@
 done
 
 lemma parts_insert_MPair [simp]:
-     "parts (insert {|X,Y|} H) =  
-          insert {|X,Y|} (parts (insert X (insert Y H)))"
+     "parts (insert \<lbrace>X,Y\<rbrace> H) =  
+          insert \<lbrace>X,Y\<rbrace> (parts (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
@@ -330,9 +326,9 @@
   analz :: "msg set => msg set"
   for H :: "msg set"
   where
-    Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
-  | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
-  | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
+    Inj [intro,simp]: "X \<in> H ==> X \<in> analz H"
+  | Fst:     "\<lbrace>X,Y\<rbrace> \<in> analz H ==> X \<in> analz H"
+  | Snd:     "\<lbrace>X,Y\<rbrace> \<in> analz H ==> Y \<in> analz H"
   | Decrypt [dest]: 
              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
 
@@ -346,7 +342,7 @@
 
 text\<open>Making it safe speeds up proofs\<close>
 lemma MPair_analz [elim!]:
-     "[| {|X,Y|} \<in> analz H;        
+     "[| \<lbrace>X,Y\<rbrace> \<in> analz H;        
              [| X \<in> analz H; Y \<in> analz H |] ==> P   
           |] ==> P"
 by (blast dest: analz.Fst analz.Snd)
@@ -427,8 +423,8 @@
 done
 
 lemma analz_insert_MPair [simp]:
-     "analz (insert {|X,Y|} H) =  
-          insert {|X,Y|} (analz (insert X (insert Y H)))"
+     "analz (insert \<lbrace>X,Y\<rbrace> H) =  
+          insert \<lbrace>X,Y\<rbrace> (analz (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule analz.induct, auto)
@@ -540,7 +536,7 @@
 
 text\<open>If there are no pairs or encryptions then analz does nothing\<close>
 lemma analz_trivial:
-     "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
+     "[| \<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
 apply safe
 apply (erule analz.induct, blast+)
 done
@@ -571,7 +567,7 @@
   | Agent  [intro]:   "Agent agt \<in> synth H"
   | Number [intro]:   "Number n  \<in> synth H"
   | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
-  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
+  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> \<lbrace>X,Y\<rbrace> \<in> synth H"
   | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
 
 text\<open>Monotonicity\<close>
@@ -585,7 +581,7 @@
  "Nonce n \<in> synth H"
  "Key K \<in> synth H"
  "Hash X \<in> synth H"
- "{|X,Y|} \<in> synth H"
+ "\<lbrace>X,Y\<rbrace> \<in> synth H"
  "Crypt K X \<in> synth H"
 
 lemma synth_increasing: "H \<subseteq> synth(H)"
@@ -694,7 +690,7 @@
 text\<open>Without this equation, other rules for synth and analz would yield
   redundant cases\<close>
 lemma MPair_synth_analz [iff]:
-     "({|X,Y|} \<in> synth (analz H)) =  
+     "(\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) =  
       (X \<in> synth (analz H) & Y \<in> synth (analz H))"
 by blast
 
@@ -706,7 +702,7 @@
 
 lemma Hash_synth_analz [simp]:
      "X \<notin> synth (analz H)  
-      ==> (Hash{|X,Y|} \<in> synth (analz H)) = (Hash{|X,Y|} \<in> analz H)"
+      ==> (Hash\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) = (Hash\<lbrace>X,Y\<rbrace> \<in> analz H)"
 by blast
 
 
@@ -742,11 +738,11 @@
 by (simp add: HPair_def)
 
 lemma MPair_eq_HPair [iff]:
-     "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
+     "(\<lbrace>X',Y'\<rbrace> = Hash[X] Y) = (X' = Hash\<lbrace>X,Y\<rbrace> & Y'=Y)"
 by (simp add: HPair_def)
 
 lemma HPair_eq_MPair [iff]:
-     "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
+     "(Hash[X] Y = \<lbrace>X',Y'\<rbrace>) = (X' = Hash\<lbrace>X,Y\<rbrace> & Y'=Y)"
 by (auto simp add: HPair_def)
 
 
@@ -757,18 +753,18 @@
 
 lemma parts_insert_HPair [simp]: 
     "parts (insert (Hash[X] Y) H) =  
-     insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"
+     insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (parts (insert Y H)))"
 by (simp add: HPair_def)
 
 lemma analz_insert_HPair [simp]: 
     "analz (insert (Hash[X] Y) H) =  
-     insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"
+     insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (analz (insert Y H)))"
 by (simp add: HPair_def)
 
 lemma HPair_synth_analz [simp]:
      "X \<notin> synth (analz H)  
     ==> (Hash[X] Y \<in> synth (analz H)) =  
-        (Hash {|X, Y|} \<in> analz H & Y \<in> synth (analz H))"
+        (Hash \<lbrace>X, Y\<rbrace> \<in> analz H & Y \<in> synth (analz H))"
 by (auto simp add: HPair_def)
 
 
@@ -814,14 +810,14 @@
   | Number: "Number N \<in> keyfree"
   | Nonce:  "Nonce N \<in> keyfree"
   | Hash:   "Hash X \<in> keyfree"
-  | MPair:  "[|X \<in> keyfree;  Y \<in> keyfree|] ==> {|X,Y|} \<in> keyfree"
+  | MPair:  "[|X \<in> keyfree;  Y \<in> keyfree|] ==> \<lbrace>X,Y\<rbrace> \<in> keyfree"
   | Crypt:  "[|X \<in> keyfree|] ==> Crypt K X \<in> keyfree"
 
 
 declare keyfree.intros [intro] 
 
 inductive_cases keyfree_KeyE: "Key K \<in> keyfree"
-inductive_cases keyfree_MPairE: "{|X,Y|} \<in> keyfree"
+inductive_cases keyfree_MPairE: "\<lbrace>X,Y\<rbrace> \<in> keyfree"
 inductive_cases keyfree_CryptE: "Crypt K X \<in> keyfree"
 
 lemma parts_keyfree: "parts (keyfree) \<subseteq> keyfree"
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/OtwayRees.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -31,17 +31,17 @@
 
          (*Alice initiates a protocol run*)
  | OR1:  "[| evs1 \<in> otway;  Nonce NA \<notin> used evs1 |]
-          ==> Says A B {|Nonce NA, Agent A, Agent B,
-                         Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
+          ==> Says A B \<lbrace>Nonce NA, Agent A, Agent B,
+                         Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace> \<rbrace>
                  # evs1 : otway"
 
          (*Bob's response to Alice's message.  Note that NB is encrypted.*)
  | OR2:  "[| evs2 \<in> otway;  Nonce NB \<notin> used evs2;
-             Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
+             Gets B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace> : set evs2 |]
           ==> Says B Server
-                  {|Nonce NA, Agent A, Agent B, X,
+                  \<lbrace>Nonce NA, Agent A, Agent B, X,
                     Crypt (shrK B)
-                      {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
+                      \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
                  # evs2 : otway"
 
          (*The Server receives Bob's message and checks that the three NAs
@@ -49,34 +49,34 @@
            forwarding to Alice.*)
  | OR3:  "[| evs3 \<in> otway;  Key KAB \<notin> used evs3;
              Gets Server
-                  {|Nonce NA, Agent A, Agent B,
-                    Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
-                    Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
+                  \<lbrace>Nonce NA, Agent A, Agent B,
+                    Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>,
+                    Crypt (shrK B) \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
                : set evs3 |]
           ==> Says Server B
-                  {|Nonce NA,
-                    Crypt (shrK A) {|Nonce NA, Key KAB|},
-                    Crypt (shrK B) {|Nonce NB, Key KAB|}|}
+                  \<lbrace>Nonce NA,
+                    Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
+                    Crypt (shrK B) \<lbrace>Nonce NB, Key KAB\<rbrace>\<rbrace>
                  # evs3 : otway"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
            those in the message he previously sent the Server.
            Need B \<noteq> Server because we allow messages to self.*)
  | OR4:  "[| evs4 \<in> otway;  B \<noteq> Server;
-             Says B Server {|Nonce NA, Agent A, Agent B, X',
+             Says B Server \<lbrace>Nonce NA, Agent A, Agent B, X',
                              Crypt (shrK B)
-                                   {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
+                                   \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
                : set evs4;
-             Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+             Gets B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
                : set evs4 |]
-          ==> Says B A {|Nonce NA, X|} # evs4 : otway"
+          ==> Says B A \<lbrace>Nonce NA, X\<rbrace> # evs4 : otway"
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.*)
  | Oops: "[| evso \<in> otway;
-             Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+             Says Server B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
                : set evso |]
-          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
+          ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso : otway"
 
 
 declare Says_imp_analz_Spy [dest]
@@ -88,7 +88,7 @@
 text\<open>A "possibility property": there are traces that reach the end\<close>
 lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
       ==> \<exists>evs \<in> otway.
-             Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
+             Says B A \<lbrace>Nonce NA, Crypt (shrK A) \<lbrace>Nonce NA, Key K\<rbrace>\<rbrace>
                \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] otway.Nil
@@ -108,12 +108,12 @@
 (** For reasoning about the encrypted portion of messages **)
 
 lemma OR2_analz_knows_Spy:
-     "[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs;  evs \<in> otway |]
+     "[| Gets B \<lbrace>N, Agent A, Agent B, X\<rbrace> \<in> set evs;  evs \<in> otway |]
       ==> X \<in> analz (knows Spy evs)"
 by blast
 
 lemma OR4_analz_knows_Spy:
-     "[| Gets B {|N, X, Crypt (shrK B) X'|} \<in> set evs;  evs \<in> otway |]
+     "[| Gets B \<lbrace>N, X, Crypt (shrK B) X'\<rbrace> \<in> set evs;  evs \<in> otway |]
       ==> X \<in> analz (knows Spy evs)"
 by blast
 
@@ -151,7 +151,7 @@
 (*Describes the form of K and NA when the Server sends this message.  Also
   for Oops case.*)
 lemma Says_Server_message_form:
-     "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+     "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
          evs \<in> otway |]
       ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
 by (erule rev_mp, erule otway.induct, simp_all)
@@ -190,8 +190,8 @@
 
 text\<open>The Key K uniquely identifies the Server's  message.\<close>
 lemma unique_session_keys:
-     "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   \<in> set evs;
-         Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs;
+     "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, K\<rbrace>\<rbrace>   \<in> set evs;
+         Says Server B' \<lbrace>NA',X',Crypt (shrK B') \<lbrace>NB',K\<rbrace>\<rbrace> \<in> set evs;
          evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"
 apply (erule rev_mp)
 apply (erule rev_mp)
@@ -205,27 +205,27 @@
 text\<open>Only OR1 can have caused such a part of a message to appear.\<close>
 lemma Crypt_imp_OR1 [rule_format]:
  "[| A \<notin> bad;  evs \<in> otway |]
-  ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
-      Says A B {|NA, Agent A, Agent B,
-                 Crypt (shrK A) {|NA, Agent A, Agent B|}|}
+  ==> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs) -->
+      Says A B \<lbrace>NA, Agent A, Agent B,
+                 Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace>
         \<in> set evs"
 by (erule otway.induct, force,
     drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 
 lemma Crypt_imp_OR1_Gets:
-     "[| Gets B {|NA, Agent A, Agent B,
-                  Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
+     "[| Gets B \<lbrace>NA, Agent A, Agent B,
+                  Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
          A \<notin> bad; evs \<in> otway |]
-       ==> Says A B {|NA, Agent A, Agent B,
-                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}
+       ==> Says A B \<lbrace>NA, Agent A, Agent B,
+                      Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace>
              \<in> set evs"
 by (blast dest: Crypt_imp_OR1)
 
 
 text\<open>The Nonce NA uniquely identifies A's message\<close>
 lemma unique_NA:
-     "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs);
-         Crypt (shrK A) {|NA, Agent A, Agent C|} \<in> parts (knows Spy evs);
+     "[| Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
+         Crypt (shrK A) \<lbrace>NA, Agent A, Agent C\<rbrace> \<in> parts (knows Spy evs);
          evs \<in> otway;  A \<notin> bad |]
       ==> B = C"
 apply (erule rev_mp, erule rev_mp)
@@ -238,9 +238,9 @@
   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   over-simplified version of this protocol: see \<open>OtwayRees_Bad\<close>.\<close>
 lemma no_nonce_OR1_OR2:
-   "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs);
+   "[| Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
        A \<notin> bad;  evs \<in> otway |]
-    ==> Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \<notin> parts (knows Spy evs)"
+    ==> Crypt (shrK A) \<lbrace>NA', NA, Agent A', Agent A\<rbrace> \<notin> parts (knows Spy evs)"
 apply (erule rev_mp)
 apply (erule otway.induct, force,
        drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
@@ -250,13 +250,13 @@
   to start a run, then it originated with the Server!\<close>
 lemma NA_Crypt_imp_Server_msg [rule_format]:
      "[| A \<notin> bad;  evs \<in> otway |]
-      ==> Says A B {|NA, Agent A, Agent B,
-                     Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs -->
-          Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs)
+      ==> Says A B \<lbrace>NA, Agent A, Agent B,
+                     Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs -->
+          Crypt (shrK A) \<lbrace>NA, Key K\<rbrace> \<in> parts (knows Spy evs)
           --> (\<exists>NB. Says Server B
-                         {|NA,
-                           Crypt (shrK A) {|NA, Key K|},
-                           Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
+                         \<lbrace>NA,
+                           Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+                           Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs)"
 apply (erule otway.induct, force,
        drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
 apply blast  \<comment>\<open>OR1: by freshness\<close>
@@ -270,14 +270,14 @@
   bad form of this protocol, even though we can prove
   \<open>Spy_not_see_encrypted_key\<close>\<close>
 lemma A_trusts_OR4:
-     "[| Says A  B {|NA, Agent A, Agent B,
-                     Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
-         Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs;
+     "[| Says A  B \<lbrace>NA, Agent A, Agent B,
+                     Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
+         Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
      A \<notin> bad;  evs \<in> otway |]
   ==> \<exists>NB. Says Server B
-               {|NA,
-                 Crypt (shrK A) {|NA, Key K|},
-                 Crypt (shrK B) {|NB, Key K|}|}
+               \<lbrace>NA,
+                 Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+                 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace>
                  \<in> set evs"
 by (blast intro!: NA_Crypt_imp_Server_msg)
 
@@ -288,9 +288,9 @@
 lemma secrecy_lemma:
  "[| A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   ==> Says Server B
-        {|NA, Crypt (shrK A) {|NA, Key K|},
-          Crypt (shrK B) {|NB, Key K|}|} \<in> set evs -->
-      Notes Spy {|NA, NB, Key K|} \<notin> set evs -->
+        \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+          Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs -->
+      Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs -->
       Key K \<notin> analz (knows Spy evs)"
 apply (erule otway.induct, force)
 apply (frule_tac [7] Says_Server_message_form)
@@ -303,9 +303,9 @@
 
 theorem Spy_not_see_encrypted_key:
      "[| Says Server B
-          {|NA, Crypt (shrK A) {|NA, Key K|},
-                Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
-         Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+          \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+                Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
+         Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
       ==> Key K \<notin> analz (knows Spy evs)"
 by (blast dest: Says_Server_message_form secrecy_lemma)
@@ -319,9 +319,9 @@
 @{term "Key K \<notin> analz (knows Spy evs)"}.\<close>
 lemma Spy_not_know_encrypted_key:
      "[| Says Server B
-          {|NA, Crypt (shrK A) {|NA, Key K|},
-                Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
-         Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+          \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+                Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
+         Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
       ==> Key K \<notin> knows Spy evs"
 by (blast dest: Spy_not_see_encrypted_key)
@@ -330,10 +330,10 @@
 text\<open>A's guarantee.  The Oops premise quantifies over NB because A cannot know
   what it is.\<close>
 lemma A_gets_good_key:
-     "[| Says A  B {|NA, Agent A, Agent B,
-                     Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
-         Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs;
-         \<forall>NB. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+     "[| Says A  B \<lbrace>NA, Agent A, Agent B,
+                     Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
+         Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
+         \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
       ==> Key K \<notin> analz (knows Spy evs)"
 by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key)
@@ -344,11 +344,11 @@
 text\<open>Only OR2 can have caused such a part of a message to appear.  We do not
   know anything about X: it does NOT have to have the right form.\<close>
 lemma Crypt_imp_OR2:
-     "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \<in> parts (knows Spy evs);
+     "[| Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);
          B \<notin> bad;  evs \<in> otway |]
       ==> \<exists>X. Says B Server
-                 {|NA, Agent A, Agent B, X,
-                   Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}
+                 \<lbrace>NA, Agent A, Agent B, X,
+                   Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
                  \<in> set evs"
 apply (erule rev_mp)
 apply (erule otway.induct, force,
@@ -358,8 +358,8 @@
 
 text\<open>The Nonce NB uniquely identifies B's  message\<close>
 lemma unique_NB:
-     "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \<in> parts(knows Spy evs);
-         Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \<in> parts(knows Spy evs);
+     "[| Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts(knows Spy evs);
+         Crypt (shrK B) \<lbrace>NC, NB, Agent C, Agent B\<rbrace> \<in> parts(knows Spy evs);
            evs \<in> otway;  B \<notin> bad |]
          ==> NC = NA & C = A"
 apply (erule rev_mp, erule rev_mp)
@@ -372,14 +372,14 @@
   then it originated with the Server!  Quite messy proof.\<close>
 lemma NB_Crypt_imp_Server_msg [rule_format]:
  "[| B \<notin> bad;  evs \<in> otway |]
-  ==> Crypt (shrK B) {|NB, Key K|} \<in> parts (knows Spy evs)
+  ==> Crypt (shrK B) \<lbrace>NB, Key K\<rbrace> \<in> parts (knows Spy evs)
       --> (\<forall>X'. Says B Server
-                     {|NA, Agent A, Agent B, X',
-                       Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}
+                     \<lbrace>NA, Agent A, Agent B, X',
+                       Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
            \<in> set evs
            --> Says Server B
-                {|NA, Crypt (shrK A) {|NA, Key K|},
-                      Crypt (shrK B) {|NB, Key K|}|}
+                \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+                      Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace>
                     \<in> set evs)"
 apply simp
 apply (erule otway.induct, force,
@@ -394,15 +394,15 @@
 text\<open>Guarantee for B: if it gets a message with matching NB then the Server
   has sent the correct message.\<close>
 theorem B_trusts_OR3:
-     "[| Says B Server {|NA, Agent A, Agent B, X',
-                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
+     "[| Says B Server \<lbrace>NA, Agent A, Agent B, X',
+                         Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
            \<in> set evs;
-         Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+         Gets B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
          B \<notin> bad;  evs \<in> otway |]
       ==> Says Server B
-               {|NA,
-                 Crypt (shrK A) {|NA, Key K|},
-                 Crypt (shrK B) {|NB, Key K|}|}
+               \<lbrace>NA,
+                 Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+                 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace>
                  \<in> set evs"
 by (blast intro!: NB_Crypt_imp_Server_msg)
 
@@ -410,11 +410,11 @@
 text\<open>The obvious combination of \<open>B_trusts_OR3\<close> with 
       \<open>Spy_not_see_encrypted_key\<close>\<close>
 lemma B_gets_good_key:
-     "[| Says B Server {|NA, Agent A, Agent B, X',
-                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
+     "[| Says B Server \<lbrace>NA, Agent A, Agent B, X',
+                         Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
            \<in> set evs;
-         Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
-         Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+         Gets B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
+         Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
       ==> Key K \<notin> analz (knows Spy evs)"
 by (blast dest!: B_trusts_OR3 Spy_not_see_encrypted_key)
@@ -422,11 +422,11 @@
 
 lemma OR3_imp_OR2:
      "[| Says Server B
-              {|NA, Crypt (shrK A) {|NA, Key K|},
-                Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+              \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+                Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
          B \<notin> bad;  evs \<in> otway |]
-  ==> \<exists>X. Says B Server {|NA, Agent A, Agent B, X,
-                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
+  ==> \<exists>X. Says B Server \<lbrace>NA, Agent A, Agent B, X,
+                            Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
               \<in> set evs"
 apply (erule rev_mp)
 apply (erule otway.induct, simp_all)
@@ -438,12 +438,12 @@
   We could probably prove that X has the expected form, but that is not
   strictly necessary for authentication.\<close>
 theorem A_auths_B:
-     "[| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs;
-         Says A  B {|NA, Agent A, Agent B,
-                     Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
+     "[| Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs;
+         Says A  B \<lbrace>NA, Agent A, Agent B,
+                     Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
-  ==> \<exists>NB X. Says B Server {|NA, Agent A, Agent B, X,
-                               Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}
+  ==> \<exists>NB X. Says B Server \<lbrace>NA, Agent A, Agent B, X,
+                               Crypt (shrK B)  \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace>
                  \<in> set evs"
 by (blast dest!: A_trusts_OR4 OR3_imp_OR2)
 
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/OtwayRees_AN.thy
--- a/src/HOL/Auth/OtwayRees_AN.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -39,30 +39,30 @@
 
  | OR1:  \<comment>\<open>Alice initiates a protocol run\<close>
          "evs1 \<in> otway
-          ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 \<in> otway"
+          ==> Says A B \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1 \<in> otway"
 
  | OR2:  \<comment>\<open>Bob's response to Alice's message.\<close>
          "[| evs2 \<in> otway;
-             Gets B {|Agent A, Agent B, Nonce NA|} \<in>set evs2 |]
-          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
+             Gets B \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in>set evs2 |]
+          ==> Says B Server \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB\<rbrace>
                  # evs2 \<in> otway"
 
  | OR3:  \<comment>\<open>The Server receives Bob's message.  Then he sends a new
            session key to Bob with a packet for forwarding to Alice.\<close>
          "[| evs3 \<in> otway;  Key KAB \<notin> used evs3;
-             Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
+             Gets Server \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB\<rbrace>
                \<in>set evs3 |]
           ==> Says Server B
-               {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
-                 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
+               \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B, Key KAB\<rbrace>,
+                 Crypt (shrK B) \<lbrace>Nonce NB, Agent A, Agent B, Key KAB\<rbrace>\<rbrace>
               # evs3 \<in> otway"
 
  | OR4:  \<comment>\<open>Bob receives the Server's (?) message and compares the Nonces with
              those in the message he previously sent the Server.
              Need @{term "B \<noteq> Server"} because we allow messages to self.\<close>
          "[| evs4 \<in> otway;  B \<noteq> Server;
-             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \<in>set evs4;
-             Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
+             Says B Server \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB\<rbrace> \<in>set evs4;
+             Gets B \<lbrace>X, Crypt(shrK B)\<lbrace>Nonce NB,Agent A,Agent B,Key K\<rbrace>\<rbrace>
                \<in>set evs4 |]
           ==> Says B A X # evs4 \<in> otway"
 
@@ -70,10 +70,10 @@
              identify the protocol run.\<close>
          "[| evso \<in> otway;
              Says Server B
-                      {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|},
-                        Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
+                      \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B, Key K\<rbrace>,
+                        Crypt (shrK B) \<lbrace>Nonce NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
                \<in>set evso |]
-          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway"
+          ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> otway"
 
 
 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
@@ -85,7 +85,7 @@
 text\<open>A "possibility property": there are traces that reach the end\<close>
 lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
       ==> \<exists>evs \<in> otway.
-           Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|})
+           Says B A (Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B, Key K\<rbrace>)
              \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] otway.Nil
@@ -104,7 +104,7 @@
 text\<open>For reasoning about the encrypted portion of messages\<close>
 
 lemma OR4_analz_knows_Spy:
-     "[| Gets B {|X, Crypt(shrK B) X'|} \<in> set evs;  evs \<in> otway |]
+     "[| Gets B \<lbrace>X, Crypt(shrK B) X'\<rbrace> \<in> set evs;  evs \<in> otway |]
       ==> X \<in> analz (knows Spy evs)"
 by blast
 
@@ -131,8 +131,8 @@
 text\<open>Describes the form of K and NA when the Server sends this message.\<close>
 lemma Says_Server_message_form:
      "[| Says Server B
-            {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
-              Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+            \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+              Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
            \<in> set evs;
          evs \<in> otway |]
       ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
@@ -175,12 +175,12 @@
 text\<open>The Key K uniquely identifies the Server's message.\<close>
 lemma unique_session_keys:
      "[| Says Server B
-          {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},
-            Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}
+          \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, K\<rbrace>,
+            Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, K\<rbrace>\<rbrace>
          \<in> set evs;
         Says Server B'
-          {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},
-            Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}
+          \<lbrace>Crypt (shrK A') \<lbrace>NA', Agent A', Agent B', K\<rbrace>,
+            Crypt (shrK B') \<lbrace>NB', Agent A', Agent B', K\<rbrace>\<rbrace>
          \<in> set evs;
         evs \<in> otway |]
      ==> A=A' & B=B' & NA=NA' & NB=NB'"
@@ -194,10 +194,10 @@
 text\<open>If the encrypted message appears then it originated with the Server!\<close>
 lemma NA_Crypt_imp_Server_msg [rule_format]:
     "[| A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
-     ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \<in> parts (knows Spy evs)
+     ==> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace> \<in> parts (knows Spy evs)
        --> (\<exists>NB. Says Server B
-                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
-                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+                    \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+                      Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
                     \<in> set evs)"
 apply (erule otway.induct, force)
 apply (simp_all add: ex_disj_distrib)
@@ -208,11 +208,11 @@
 text\<open>Corollary: if A receives B's OR4 message then it originated with the
       Server. Freshness may be inferred from nonce NA.\<close>
 lemma A_trusts_OR4:
-     "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \<in> set evs;
+     "[| Says B' A (Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>) \<in> set evs;
          A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
       ==> \<exists>NB. Says Server B
-                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
-                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+                  \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+                    Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
                  \<in> set evs"
 by (blast intro!: NA_Crypt_imp_Server_msg)
 
@@ -223,10 +223,10 @@
 lemma secrecy_lemma:
      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
       ==> Says Server B
-           {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
-             Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+           \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+             Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
           \<in> set evs -->
-          Notes Spy {|NA, NB, Key K|} \<notin> set evs -->
+          Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs -->
           Key K \<notin> analz (knows Spy evs)"
 apply (erule otway.induct, force)
 apply (frule_tac [7] Says_Server_message_form)
@@ -239,10 +239,10 @@
 
 lemma Spy_not_see_encrypted_key:
      "[| Says Server B
-            {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
-              Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+            \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+              Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
            \<in> set evs;
-         Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+         Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
       ==> Key K \<notin> analz (knows Spy evs)"
   by (metis secrecy_lemma)
@@ -251,8 +251,8 @@
 text\<open>A's guarantee.  The Oops premise quantifies over NB because A cannot know
   what it is.\<close>
 lemma A_gets_good_key:
-     "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \<in> set evs;
-         \<forall>NB. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+     "[| Says B' A (Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>) \<in> set evs;
+         \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
       ==> Key K \<notin> analz (knows Spy evs)"
   by (metis A_trusts_OR4 secrecy_lemma)
@@ -264,10 +264,10 @@
 text\<open>If the encrypted message appears then it originated with the Server!\<close>
 lemma NB_Crypt_imp_Server_msg [rule_format]:
  "[| B \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
-  ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \<in> parts (knows Spy evs)
+  ==> Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace> \<in> parts (knows Spy evs)
       --> (\<exists>NA. Says Server B
-                   {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
-                     Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+                   \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+                     Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
                    \<in> set evs)"
 apply (erule otway.induct, force, simp_all add: ex_disj_distrib)
 apply blast+  \<comment>\<open>Fake, OR3\<close>
@@ -278,12 +278,12 @@
 text\<open>Guarantee for B: if it gets a well-formed certificate then the Server
   has sent the correct message in round 3.\<close>
 lemma B_trusts_OR3:
-     "[| Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+     "[| Says S B \<lbrace>X, Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
            \<in> set evs;
          B \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
       ==> \<exists>NA. Says Server B
-                   {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
-                     Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+                   \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
+                     Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
                    \<in> set evs"
 by (blast intro!: NB_Crypt_imp_Server_msg)
 
@@ -291,9 +291,9 @@
 text\<open>The obvious combination of \<open>B_trusts_OR3\<close> with 
       \<open>Spy_not_see_encrypted_key\<close>\<close>
 lemma B_gets_good_key:
-     "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+     "[| Gets B \<lbrace>X, Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
           \<in> set evs;
-         \<forall>NA. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+         \<forall>NA. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
       ==> Key K \<notin> analz (knows Spy evs)"
 by (blast dest: B_trusts_OR3 Spy_not_see_encrypted_key)
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -36,17 +36,17 @@
 
  | OR1:  \<comment>\<open>Alice initiates a protocol run\<close>
          "[| evs1 \<in> otway;  Nonce NA \<notin> used evs1 |]
-          ==> Says A B {|Nonce NA, Agent A, Agent B,
-                         Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
+          ==> Says A B \<lbrace>Nonce NA, Agent A, Agent B,
+                         Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace>
                  # evs1 \<in> otway"
 
  | OR2:  \<comment>\<open>Bob's response to Alice's message.
              This variant of the protocol does NOT encrypt NB.\<close>
          "[| evs2 \<in> otway;  Nonce NB \<notin> used evs2;
-             Gets B {|Nonce NA, Agent A, Agent B, X|} \<in> set evs2 |]
+             Gets B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace> \<in> set evs2 |]
           ==> Says B Server
-                  {|Nonce NA, Agent A, Agent B, X, Nonce NB,
-                    Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
+                  \<lbrace>Nonce NA, Agent A, Agent B, X, Nonce NB,
+                    Crypt (shrK B) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace>
                  # evs2 \<in> otway"
 
  | OR3:  \<comment>\<open>The Server receives Bob's message and checks that the three NAs
@@ -54,34 +54,34 @@
            forwarding to Alice.\<close>
          "[| evs3 \<in> otway;  Key KAB \<notin> used evs3;
              Gets Server
-                  {|Nonce NA, Agent A, Agent B,
-                    Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
+                  \<lbrace>Nonce NA, Agent A, Agent B,
+                    Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>,
                     Nonce NB,
-                    Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
+                    Crypt (shrK B) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace>
                \<in> set evs3 |]
           ==> Says Server B
-                  {|Nonce NA,
-                    Crypt (shrK A) {|Nonce NA, Key KAB|},
-                    Crypt (shrK B) {|Nonce NB, Key KAB|}|}
+                  \<lbrace>Nonce NA,
+                    Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
+                    Crypt (shrK B) \<lbrace>Nonce NB, Key KAB\<rbrace>\<rbrace>
                  # evs3 \<in> otway"
 
  | OR4:  \<comment>\<open>Bob receives the Server's (?) message and compares the Nonces with
              those in the message he previously sent the Server.
              Need @{term "B \<noteq> Server"} because we allow messages to self.\<close>
          "[| evs4 \<in> otway;  B \<noteq> Server;
-             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
-                             Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
+             Says B Server \<lbrace>Nonce NA, Agent A, Agent B, X', Nonce NB,
+                             Crypt (shrK B) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace>
                \<in> set evs4;
-             Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+             Gets B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
                \<in> set evs4 |]
-          ==> Says B A {|Nonce NA, X|} # evs4 \<in> otway"
+          ==> Says B A \<lbrace>Nonce NA, X\<rbrace> # evs4 \<in> otway"
 
  | Oops: \<comment>\<open>This message models possible leaks of session keys.  The nonces
              identify the protocol run.\<close>
          "[| evso \<in> otway;
-             Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+             Says Server B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
                \<in> set evso |]
-          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway"
+          ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> otway"
 
 
 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
@@ -92,7 +92,7 @@
 text\<open>A "possibility property": there are traces that reach the end\<close>
 lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
       ==> \<exists>NA. \<exists>evs \<in> otway.
-            Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
+            Says B A \<lbrace>Nonce NA, Crypt (shrK A) \<lbrace>Nonce NA, Key K\<rbrace>\<rbrace>
               \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] otway.Nil
@@ -112,17 +112,17 @@
 subsection\<open>For reasoning about the encrypted portion of messages\<close>
 
 lemma OR2_analz_knows_Spy:
-     "[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs;  evs \<in> otway |]
+     "[| Gets B \<lbrace>N, Agent A, Agent B, X\<rbrace> \<in> set evs;  evs \<in> otway |]
       ==> X \<in> analz (knows Spy evs)"
 by blast
 
 lemma OR4_analz_knows_Spy:
-     "[| Gets B {|N, X, Crypt (shrK B) X'|} \<in> set evs;  evs \<in> otway |]
+     "[| Gets B \<lbrace>N, X, Crypt (shrK B) X'\<rbrace> \<in> set evs;  evs \<in> otway |]
       ==> X \<in> analz (knows Spy evs)"
 by blast
 
 lemma Oops_parts_knows_Spy:
-     "Says Server B {|NA, X, Crypt K' {|NB,K|}|} \<in> set evs
+     "Says Server B \<lbrace>NA, X, Crypt K' \<lbrace>NB,K\<rbrace>\<rbrace> \<in> set evs
       ==> K \<in> parts (knows Spy evs)"
 by blast
 
@@ -155,7 +155,7 @@
 text\<open>Describes the form of K and NA when the Server sends this message.  Also
   for Oops case.\<close>
 lemma Says_Server_message_form:
-     "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+     "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
          evs \<in> otway |]
       ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
 apply (erule rev_mp)
@@ -196,8 +196,8 @@
 
 text\<open>The Key K uniquely identifies the Server's  message.\<close>
 lemma unique_session_keys:
-     "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   \<in> set evs;
-         Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs;
+     "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, K\<rbrace>\<rbrace>   \<in> set evs;
+         Says Server B' \<lbrace>NA',X',Crypt (shrK B') \<lbrace>NB',K\<rbrace>\<rbrace> \<in> set evs;
          evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"
 apply (erule rev_mp)
 apply (erule rev_mp)
@@ -212,9 +212,9 @@
 lemma secrecy_lemma:
  "[| A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   ==> Says Server B
-        {|NA, Crypt (shrK A) {|NA, Key K|},
-          Crypt (shrK B) {|NB, Key K|}|} \<in> set evs -->
-      Notes Spy {|NA, NB, Key K|} \<notin> set evs -->
+        \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+          Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs -->
+      Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs -->
       Key K \<notin> analz (knows Spy evs)"
 apply (erule otway.induct, force)
 apply (frule_tac [7] Says_Server_message_form)
@@ -228,9 +228,9 @@
 
 lemma Spy_not_see_encrypted_key:
      "[| Says Server B
-          {|NA, Crypt (shrK A) {|NA, Key K|},
-                Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
-         Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+          \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+                Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs;
+         Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
       ==> Key K \<notin> analz (knows Spy evs)"
 by (blast dest: Says_Server_message_form secrecy_lemma)
@@ -243,9 +243,9 @@
   up. Original Otway-Rees doesn't need it.\<close>
 lemma Crypt_imp_OR1 [rule_format]:
      "[| A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
-      ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
-          Says A B {|NA, Agent A, Agent B,
-                     Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \<in> set evs"
+      ==> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs) -->
+          Says A B \<lbrace>NA, Agent A, Agent B,
+                     Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace>  \<in> set evs"
 by (erule otway.induct, force,
     drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 
@@ -256,14 +256,14 @@
 text\<open>Only it is FALSE.  Somebody could make a fake message to Server
           substituting some other nonce NA' for NB.\<close>
 lemma "[| A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
-       ==> Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs) -->
-           Says A B {|NA, Agent A, Agent B,
-                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}
+       ==> Crypt (shrK A) \<lbrace>NA, Key K\<rbrace> \<in> parts (knows Spy evs) -->
+           Says A B \<lbrace>NA, Agent A, Agent B,
+                      Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace>
             \<in> set evs -->
            (\<exists>B NB. Says Server B
-                {|NA,
-                  Crypt (shrK A) {|NA, Key K|},
-                  Crypt (shrK B) {|NB, Key K|}|}  \<in> set evs)"
+                \<lbrace>NA,
+                  Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>,
+                  Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs)"
 apply (erule otway.induct, force,
        drule_tac [4] OR2_parts_knows_Spy, simp_all)
 apply blast  \<comment>\<open>Fake\<close>
@@ -276,13 +276,13 @@
 (*The hypotheses at this point suggest an attack in which nonce NB is used
   in two different roles:
           Gets Server
-           {|Nonce NA, Agent Aa, Agent A,
-             Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB,
-             Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|}
+           \<lbrace>Nonce NA, Agent Aa, Agent A,
+             Crypt (shrK Aa) \<lbrace>Nonce NA, Agent Aa, Agent A\<rbrace>, Nonce NB,
+             Crypt (shrK A) \<lbrace>Nonce NA, Agent Aa, Agent A\<rbrace>\<rbrace>
           \<in> set evs3
           Says A B
-           {|Nonce NB, Agent A, Agent B,
-             Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|}
+           \<lbrace>Nonce NB, Agent A, Agent B,
+             Crypt (shrK A) \<lbrace>Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
           \<in> set evs3;
 *)
 
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Public.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -239,13 +239,13 @@
 apply (auto dest!: parts_cut simp add: used_Nil) 
 done
 
-lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"
+lemma MPair_used_D: "\<lbrace>X,Y\<rbrace> \<in> used H ==> X \<in> used H & Y \<in> used H"
 by (drule used_parts_subset_parts, simp, blast)
 
 text\<open>There was a similar theorem in Event.thy, so perhaps this one can
   be moved up if proved directly by induction.\<close>
 lemma MPair_used [elim!]:
-     "[| {|X,Y|} \<in> used H;
+     "[| \<lbrace>X,Y\<rbrace> \<in> used H;
          [| X \<in> used H; Y \<in> used H |] ==> P |] 
       ==> P"
 by (blast dest: MPair_used_D) 
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Recur.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -21,18 +21,18 @@
   for evs :: "event list"
   where
    One:  "Key KAB \<notin> used evs
-          ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|},
-               {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|},
+          ==> (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>,
+               \<lbrace>Crypt (shrK A) \<lbrace>Key KAB, Agent B, Nonce NA\<rbrace>, END\<rbrace>,
                KAB)   \<in> respond evs"
 
     (*The most recent session key is passed up to the caller*)
  | Cons: "[| (PA, RA, KAB) \<in> respond evs;
              Key KBC \<notin> used evs;  Key KBC \<notin> parts {RA};
-             PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} |]
-          ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|},
-               {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
-                 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
-                 RA|},
+             PA = Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, P\<rbrace> |]
+          ==> (Hash[Key(shrK B)] \<lbrace>Agent B, Agent C, Nonce NB, PA\<rbrace>,
+               \<lbrace>Crypt (shrK B) \<lbrace>Key KBC, Agent C, Nonce NB\<rbrace>,
+                 Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>,
+                 RA\<rbrace>,
                KBC)
               \<in> respond evs"
 
@@ -48,8 +48,8 @@
    Nil:  "END \<in> responses evs"
 
  | Cons: "[| RA \<in> responses evs;  Key KAB \<notin> used evs |]
-          ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
-                RA|}  \<in> responses evs"
+          ==> \<lbrace>Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>,
+                RA\<rbrace>  \<in> responses evs"
 
 
 inductive_set recur :: "event list set"
@@ -65,15 +65,15 @@
          (*Alice initiates a protocol run.
            END is a placeholder to terminate the nesting.*)
  | RA1:  "[| evs1 \<in> recur;  Nonce NA \<notin> used evs1 |]
-          ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|})
+          ==> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>)
               # evs1 \<in> recur"
 
          (*Bob's response to Alice's message.  C might be the Server.
-           We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because
+           We omit PA = \<lbrace>XA, Agent A, Agent B, Nonce NA, P\<rbrace> because
            it complicates proofs, so B may respond to any message at all!*)
  | RA2:  "[| evs2 \<in> recur;  Nonce NB \<notin> used evs2;
              Says A' B PA \<in> set evs2 |]
-          ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
+          ==> Says B C (Hash[Key(shrK B)] \<lbrace>Agent B, Agent C, Nonce NB, PA\<rbrace>)
               # evs2 \<in> recur"
 
          (*The Server receives Bob's message and prepares a response.*)
@@ -84,11 +84,11 @@
          (*Bob receives the returned message and compares the Nonces with
            those in the message he previously sent the Server.*)
  | RA4:  "[| evs4 \<in> recur;
-             Says B  C {|XH, Agent B, Agent C, Nonce NB,
-                         XA, Agent A, Agent B, Nonce NA, P|} \<in> set evs4;
-             Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
-                         Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
-                         RA|} \<in> set evs4 |]
+             Says B  C \<lbrace>XH, Agent B, Agent C, Nonce NB,
+                         XA, Agent A, Agent B, Nonce NA, P\<rbrace> \<in> set evs4;
+             Says C' B \<lbrace>Crypt (shrK B) \<lbrace>Key KBC, Agent C, Nonce NB\<rbrace>,
+                         Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>,
+                         RA\<rbrace> \<in> set evs4 |]
           ==> Says B A RA # evs4 \<in> recur"
 
    (*No "oops" message can easily be expressed.  Each session key is
@@ -101,7 +101,7 @@
 
    Oops:  "[| evso \<in> recur;  Says Server B RB \<in> set evso;
               RB \<in> responses evs';  Key K \<in> parts {RB} |]
-           ==> Notes Spy {|Key K, RB|} # evso \<in> recur"
+           ==> Notes Spy \<lbrace>Key K, RB\<rbrace> # evso \<in> recur"
   *)
 
 
@@ -120,8 +120,8 @@
 text\<open>Simplest case: Alice goes directly to the server\<close>
 lemma "Key K \<notin> used [] 
        ==> \<exists>NA. \<exists>evs \<in> recur.
-              Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
-                    END|}  \<in> set evs"
+              Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent Server, Nonce NA\<rbrace>,
+                    END\<rbrace>  \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] recur.Nil [THEN recur.RA1, 
                              THEN recur.RA3 [OF _ _ respond.One]])
@@ -133,8 +133,8 @@
 lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K';
           Nonce NA \<notin> used []; Nonce NB \<notin> used []; NA < NB |]
        ==> \<exists>NA. \<exists>evs \<in> recur.
-        Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
-                   END|}  \<in> set evs"
+        Says B A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent B, Nonce NA\<rbrace>,
+                   END\<rbrace>  \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] 
           recur.Nil
@@ -152,8 +152,8 @@
           Nonce NA \<notin> used []; Nonce NB \<notin> used []; Nonce NC \<notin> used []; 
           NA < NB; NB < NC |]
        ==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
-             Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
-                        END|}  \<in> set evs"
+             Says B A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent B, Nonce NA\<rbrace>,
+                        END\<rbrace>  \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] 
           recur.Nil [THEN recur.RA1, 
@@ -189,7 +189,7 @@
 lemmas RA2_analz_spies = Says_imp_spies [THEN analz.Inj]
 
 lemma RA4_analz_spies:
-     "Says C' B {|Crypt K X, X', RA|} \<in> set evs ==> RA \<in> analz (spies evs)"
+     "Says C' B \<lbrace>Crypt K X, X', RA\<rbrace> \<in> set evs ==> RA \<in> analz (spies evs)"
 by blast
 
 
@@ -278,7 +278,7 @@
 
 text\<open>Everything that's hashed is already in past traffic.\<close>
 lemma Hash_imp_body:
-     "[| Hash {|Key(shrK A), X|} \<in> parts (spies evs);
+     "[| Hash \<lbrace>Key(shrK A), X\<rbrace> \<in> parts (spies evs);
          evs \<in> recur;  A \<notin> bad |] ==> X \<in> parts (spies evs)"
 apply (erule rev_mp)
 apply (erule recur.induct,
@@ -299,8 +299,8 @@
 **)
 
 lemma unique_NA:
-  "[| Hash {|Key(shrK A), Agent A, B, NA, P|} \<in> parts (spies evs);
-      Hash {|Key(shrK A), Agent A, B',NA, P'|} \<in> parts (spies evs);
+  "[| Hash \<lbrace>Key(shrK A), Agent A, B, NA, P\<rbrace> \<in> parts (spies evs);
+      Hash \<lbrace>Key(shrK A), Agent A, B',NA, P'\<rbrace> \<in> parts (spies evs);
       evs \<in> recur;  A \<notin> bad |]
     ==> B=B' & P=P'"
 apply (erule rev_mp, erule rev_mp)
@@ -348,8 +348,8 @@
 
 text\<open>The last key returned by respond indeed appears in a certificate\<close>
 lemma respond_certificate:
-     "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \<in> respond evs
-      ==> Crypt (shrK A) {|Key K, B, NA|} \<in> parts {RA}"
+     "(Hash[Key(shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, RA, K) \<in> respond evs
+      ==> Crypt (shrK A) \<lbrace>Key K, B, NA\<rbrace> \<in> parts {RA}"
 apply (ind_cases "(Hash[Key (shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, RA, K) \<in> respond evs")
 apply simp_all
 done
@@ -361,8 +361,8 @@
   the quantifiers appear to be necessary.*)
 lemma unique_lemma [rule_format]:
      "(PB,RB,KXY) \<in> respond evs ==>
-      \<forall>A B N. Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB} -->
-      (\<forall>A' B' N'. Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB} -->
+      \<forall>A B N. Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB} -->
+      (\<forall>A' B' N'. Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB} -->
       (A'=A & B'=B) | (A'=B & B'=A))"
 apply (erule respond.induct)
 apply (simp_all add: all_conj_distrib)
@@ -370,8 +370,8 @@
 done
 
 lemma unique_session_keys:
-     "[| Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB};
-         Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB};
+     "[| Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB};
+         Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB};
          (PB,RB,KXY) \<in> respond evs |]
       ==> (A'=A & B'=B) | (A'=B & B'=A)"
 by (rule unique_lemma, auto)
@@ -384,7 +384,7 @@
 lemma respond_Spy_not_see_session_key [rule_format]:
      "[| (PB,RB,KAB) \<in> respond evs;  evs \<in> recur |]
       ==> \<forall>A A' N. A \<notin> bad & A' \<notin> bad -->
-          Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts{RB} -->
+          Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<in> parts{RB} -->
           Key K \<notin> analz (insert RB (spies evs))"
 apply (erule respond.induct)
 apply (frule_tac [2] respond_imp_responses)
@@ -405,7 +405,7 @@
 
 
 lemma Spy_not_see_session_key:
-     "[| Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts (spies evs);
+     "[| Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<in> parts (spies evs);
          A \<notin> bad;  A' \<notin> bad;  evs \<in> recur |]
       ==> Key K \<notin> analz (spies evs)"
 apply (erule rev_mp)
@@ -430,9 +430,9 @@
 
 text\<open>The response never contains Hashes\<close>
 lemma Hash_in_parts_respond:
-     "[| Hash {|Key (shrK B), M|} \<in> parts (insert RB H);
+     "[| Hash \<lbrace>Key (shrK B), M\<rbrace> \<in> parts (insert RB H);
          (PB,RB,K) \<in> respond evs |]
-      ==> Hash {|Key (shrK B), M|} \<in> parts H"
+      ==> Hash \<lbrace>Key (shrK B), M\<rbrace> \<in> parts H"
 apply (erule rev_mp)
 apply (erule respond_imp_responses [THEN responses.induct], auto)
 done
@@ -442,9 +442,9 @@
   it can say nothing about how recent A's message is.  It might later be
   used to prove B's presence to A at the run's conclusion.\<close>
 lemma Hash_auth_sender [rule_format]:
-     "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \<in> parts(spies evs);
+     "[| Hash \<lbrace>Key(shrK A), Agent A, Agent B, NA, P\<rbrace> \<in> parts(spies evs);
          A \<notin> bad;  evs \<in> recur |]
-      ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \<in> set evs"
+      ==> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, NA, P\<rbrace>) \<in> set evs"
 apply (unfold HPair_def)
 apply (erule rev_mp)
 apply (erule recur.induct,
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/TLS.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -20,7 +20,7 @@
 The model assumes that no fraudulent certificates are present, but it does
 assume that some private keys are to the spy.
 
-REMARK.  The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientKeyExch,
+REMARK.  The event "Notes A \<lbrace>Agent B, Nonce PMS\<rbrace>" appears in ClientKeyExch,
 CertVerify, ClientFinished to record that A knows M.  It is a note from A to
 herself.  Nobody else can see it.  In ClientKeyExch, the Spy can substitute
 his own certificate for A's, but he cannot replace A's note by one for himself.
@@ -35,7 +35,7 @@
 Proofs would be simpler if ClientKeyExch included A's name within
 Crypt KB (Nonce PMS).  As things stand, there is much overlap between proofs
 about that message (which B receives) and the stronger event
-Notes A {|Agent B, Nonce PMS|}.
+Notes A \<lbrace>Agent B, Nonce PMS\<rbrace>.
 *)
 
 section\<open>The TLS Protocol: Transport Layer Security\<close>
@@ -43,7 +43,7 @@
 theory TLS imports Public "~~/src/HOL/Library/Nat_Bijection" begin
 
 definition certificate :: "[agent,key] => msg" where
-    "certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}"
+    "certificate A KA == Crypt (priSK Server) \<lbrace>Agent A, Key KA\<rbrace>"
 
 text\<open>TLS apparently does not require separate keypairs for encryption and
 signature.  Therefore, we formalize signature as encryption using the
@@ -109,8 +109,8 @@
                 to available nonces\<close>
          "[| evsSK \<in> tls;
              {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
-          ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
-                           Key (sessionK((NA,NB,M),role)) |} # evsSK \<in> tls"
+          ==> Notes Spy \<lbrace> Nonce (PRF(M,NA,NB)),
+                           Key (sessionK((NA,NB,M),role))\<rbrace> # evsSK \<in> tls"
 
  | ClientHello:
          \<comment>\<open>(7.4.1.2)
@@ -121,7 +121,7 @@
            May assume @{term "NA \<notin> range PRF"} because CLIENT RANDOM is 
            28 bytes while MASTER SECRET is 48 bytes\<close>
          "[| evsCH \<in> tls;  Nonce NA \<notin> used evsCH;  NA \<notin> range PRF |]
-          ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
+          ==> Says A B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
                 # evsCH  \<in>  tls"
 
  | ServerHello:
@@ -130,9 +130,9 @@
            SERVER CERTIFICATE (7.4.2) is always present.
            \<open>CERTIFICATE_REQUEST\<close> (7.4.4) is implied.\<close>
          "[| evsSH \<in> tls;  Nonce NB \<notin> used evsSH;  NB \<notin> range PRF;
-             Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
+             Says A' B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
                \<in> set evsSH |]
-          ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH  \<in>  tls"
+          ==> Says B A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> # evsSH  \<in>  tls"
 
  | Certificate:
          \<comment>\<open>SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.\<close>
@@ -150,7 +150,7 @@
          "[| evsCX \<in> tls;  Nonce PMS \<notin> used evsCX;  PMS \<notin> range PRF;
              Says B' A (certificate B KB) \<in> set evsCX |]
           ==> Says A B (Crypt KB (Nonce PMS))
-              # Notes A {|Agent B, Nonce PMS|}
+              # Notes A \<lbrace>Agent B, Nonce PMS\<rbrace>
               # evsCX  \<in>  tls"
 
  | CertVerify:
@@ -160,9 +160,9 @@
           Checking the signature, which is the only use of A's certificate,
           assures B of A's presence\<close>
          "[| evsCV \<in> tls;
-             Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCV;
-             Notes A {|Agent B, Nonce PMS|} \<in> set evsCV |]
-          ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
+             Says B' A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsCV;
+             Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCV |]
+          ==> Says A B (Crypt (priK A) (Hash\<lbrace>Nonce NB, Agent B, Nonce PMS\<rbrace>))
               # evsCV  \<in>  tls"
 
         \<comment>\<open>Finally come the FINISHED messages (7.4.8), confirming PA and PB
@@ -170,37 +170,37 @@
           Either party may send its message first.\<close>
 
  | ClientFinished:
-        \<comment>\<open>The occurrence of Notes A {|Agent B, Nonce PMS|} stops the
+        \<comment>\<open>The occurrence of Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> stops the
           rule's applying when the Spy has satisfied the "Says A B" by
           repaying messages sent by the true client; in that case, the
           Spy does not know PMS and could not send ClientFinished.  One
           could simply put @{term "A\<noteq>Spy"} into the rule, but one should not
           expect the spy to be well-behaved.\<close>
          "[| evsCF \<in> tls;
-             Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
+             Says A  B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
                \<in> set evsCF;
-             Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCF;
-             Notes A {|Agent B, Nonce PMS|} \<in> set evsCF;
+             Says B' A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsCF;
+             Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCF;
              M = PRF(PMS,NA,NB) |]
           ==> Says A B (Crypt (clientK(NA,NB,M))
-                        (Hash{|Number SID, Nonce M,
+                        (Hash\<lbrace>Number SID, Nonce M,
                                Nonce NA, Number PA, Agent A,
-                               Nonce NB, Number PB, Agent B|}))
+                               Nonce NB, Number PB, Agent B\<rbrace>))
               # evsCF  \<in>  tls"
 
  | ServerFinished:
         \<comment>\<open>Keeping A' and A'' distinct means B cannot even check that the
           two messages originate from the same source.\<close>
          "[| evsSF \<in> tls;
-             Says A' B  {|Agent A, Nonce NA, Number SID, Number PA|}
+             Says A' B  \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>
                \<in> set evsSF;
-             Says B  A  {|Nonce NB, Number SID, Number PB|} \<in> set evsSF;
+             Says B  A  \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsSF;
              Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSF;
              M = PRF(PMS,NA,NB) |]
           ==> Says B A (Crypt (serverK(NA,NB,M))
-                        (Hash{|Number SID, Nonce M,
+                        (Hash\<lbrace>Number SID, Nonce M,
                                Nonce NA, Number PA, Agent A,
-                               Nonce NB, Number PB, Agent B|}))
+                               Nonce NB, Number PB, Agent B\<rbrace>))
               # evsSF  \<in>  tls"
 
  | ClientAccepts:
@@ -209,15 +209,15 @@
           needed to resume this session.  The "Notes A ..." premise is
           used to prove \<open>Notes_master_imp_Crypt_PMS\<close>.\<close>
          "[| evsCA \<in> tls;
-             Notes A {|Agent B, Nonce PMS|} \<in> set evsCA;
+             Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evsCA;
              M = PRF(PMS,NA,NB);
-             X = Hash{|Number SID, Nonce M,
+             X = Hash\<lbrace>Number SID, Nonce M,
                        Nonce NA, Number PA, Agent A,
-                       Nonce NB, Number PB, Agent B|};
+                       Nonce NB, Number PB, Agent B\<rbrace>;
              Says A  B (Crypt (clientK(NA,NB,M)) X) \<in> set evsCA;
              Says B' A (Crypt (serverK(NA,NB,M)) X) \<in> set evsCA |]
           ==>
-             Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA  \<in>  tls"
+             Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> # evsCA  \<in>  tls"
 
  | ServerAccepts:
         \<comment>\<open>Having transmitted ServerFinished and received an identical
@@ -228,38 +228,38 @@
              A \<noteq> B;
              Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSA;
              M = PRF(PMS,NA,NB);
-             X = Hash{|Number SID, Nonce M,
+             X = Hash\<lbrace>Number SID, Nonce M,
                        Nonce NA, Number PA, Agent A,
-                       Nonce NB, Number PB, Agent B|};
+                       Nonce NB, Number PB, Agent B\<rbrace>;
              Says B  A (Crypt (serverK(NA,NB,M)) X) \<in> set evsSA;
              Says A' B (Crypt (clientK(NA,NB,M)) X) \<in> set evsSA |]
           ==>
-             Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  \<in>  tls"
+             Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> # evsSA  \<in>  tls"
 
  | ClientResume:
          \<comment>\<open>If A recalls the \<open>SESSION_ID\<close>, then she sends a FINISHED
              message using the new nonces and stored MASTER SECRET.\<close>
          "[| evsCR \<in> tls;
-             Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
-             Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCR;
-             Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evsCR |]
+             Says A  B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>: set evsCR;
+             Says B' A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsCR;
+             Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evsCR |]
           ==> Says A B (Crypt (clientK(NA,NB,M))
-                        (Hash{|Number SID, Nonce M,
+                        (Hash\<lbrace>Number SID, Nonce M,
                                Nonce NA, Number PA, Agent A,
-                               Nonce NB, Number PB, Agent B|}))
+                               Nonce NB, Number PB, Agent B\<rbrace>))
               # evsCR  \<in>  tls"
 
  | ServerResume:
          \<comment>\<open>Resumption (7.3):  If B finds the \<open>SESSION_ID\<close> then he can 
              send a FINISHED message using the recovered MASTER SECRET\<close>
          "[| evsSR \<in> tls;
-             Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
-             Says B  A {|Nonce NB, Number SID, Number PB|} \<in> set evsSR;
-             Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evsSR |]
+             Says A' B \<lbrace>Agent A, Nonce NA, Number SID, Number PA\<rbrace>: set evsSR;
+             Says B  A \<lbrace>Nonce NB, Number SID, Number PB\<rbrace> \<in> set evsSR;
+             Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evsSR |]
           ==> Says B A (Crypt (serverK(NA,NB,M))
-                        (Hash{|Number SID, Nonce M,
+                        (Hash\<lbrace>Number SID, Nonce M,
                                Nonce NA, Number PA, Agent A,
-                               Nonce NB, Number PB, Agent B|})) # evsSR
+                               Nonce NB, Number PB, Agent B\<rbrace>)) # evsSR
                 \<in>  tls"
 
  | Oops:
@@ -333,7 +333,7 @@
 text\<open>Possibility property ending with ClientAccepts.\<close>
 lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF;  A \<noteq> B |]
       ==> \<exists>SID M. \<exists>evs \<in> tls.
-            Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs"
+            Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] tls.Nil
                     [THEN tls.ClientHello, THEN tls.ServerHello,
@@ -346,7 +346,7 @@
 text\<open>And one for ServerAccepts.  Either FINISHED message may come first.\<close>
 lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |]
       ==> \<exists>SID NA PA NB PB M. \<exists>evs \<in> tls.
-           Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs"
+           Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] tls.Nil
                     [THEN tls.ClientHello, THEN tls.ServerHello,
@@ -359,7 +359,7 @@
 text\<open>Another one, for CertVerify (which is optional)\<close>
 lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF;  A \<noteq> B |]
        ==> \<exists>NB PMS. \<exists>evs \<in> tls.
-              Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) 
+              Says A B (Crypt (priK A) (Hash\<lbrace>Nonce NB, Agent B, Nonce PMS\<rbrace>)) 
                 \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] tls.Nil
@@ -372,14 +372,14 @@
 text\<open>Another one, for session resumption (both ServerResume and ClientResume).
   NO tls.Nil here: we refer to a previous session, not the empty trace.\<close>
 lemma "[| evs0 \<in> tls;
-          Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0;
-          Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0;
+          Notes A \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs0;
+          Notes B \<lbrace>Number SID, Agent A, Agent B, Nonce M\<rbrace> \<in> set evs0;
           \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF;
           A \<noteq> B |]
       ==> \<exists>NA PA NB PB X. \<exists>evs \<in> tls.
-                X = Hash{|Number SID, Nonce M,
+                X = Hash\<lbrace>Number SID, Nonce M,
                           Nonce NA, Number PA, Agent A,
-                          Nonce NB, Number PB, Agent B|}  &
+                          Nonce NB, Number PB, Agent B\<rbrace>  &
                 Says A B (Crypt (clientK(NA,NB,M)) X) \<in> set evs  &
                 Says B A (Crypt (serverK(NA,NB,M)) X) \<in> set evs"
 apply (intro exI bexI)
@@ -425,7 +425,7 @@
 subsubsection\<open>Properties of items found in Notes\<close>
 
 lemma Notes_Crypt_parts_spies:
-     "[| Notes A {|Agent B, X|} \<in> set evs;  evs \<in> tls |]
+     "[| Notes A \<lbrace>Agent B, X\<rbrace> \<in> set evs;  evs \<in> tls |]
       ==> Crypt (pubK B) X \<in> parts (spies evs)"
 apply (erule rev_mp)
 apply (erule tls.induct, 
@@ -435,7 +435,7 @@
 
 text\<open>C may be either A or B\<close>
 lemma Notes_master_imp_Crypt_PMS:
-     "[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs;
+     "[| Notes C \<lbrace>s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))\<rbrace> \<in> set evs;
          evs \<in> tls |]
       ==> Crypt (pubK B) (Nonce PMS) \<in> parts (spies evs)"
 apply (erule rev_mp)
@@ -448,9 +448,9 @@
 
 text\<open>Compared with the theorem above, both premise and conclusion are stronger\<close>
 lemma Notes_master_imp_Notes_PMS:
-     "[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs;
+     "[| Notes A \<lbrace>s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))\<rbrace> \<in> set evs;
          evs \<in> tls |]
-      ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
+      ==> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs"
 apply (erule rev_mp)
 apply (erule tls.induct, force, simp_all)
 txt\<open>ServerAccepts\<close>
@@ -463,7 +463,7 @@
 text\<open>B can check A's signature if he has received A's certificate.\<close>
 lemma TrustCertVerify_lemma:
      "[| X \<in> parts (spies evs);
-         X = Crypt (priK A) (Hash{|nb, Agent B, pms|});
+         X = Crypt (priK A) (Hash\<lbrace>nb, Agent B, pms\<rbrace>);
          evs \<in> tls;  A \<notin> bad |]
       ==> Says A B X \<in> set evs"
 apply (erule rev_mp, erule ssubst)
@@ -473,7 +473,7 @@
 text\<open>Final version: B checks X using the distributed KA instead of priK A\<close>
 lemma TrustCertVerify:
      "[| X \<in> parts (spies evs);
-         X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|});
+         X = Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, pms\<rbrace>);
          certificate A KA \<in> parts (spies evs);
          evs \<in> tls;  A \<notin> bad |]
       ==> Says A B X \<in> set evs"
@@ -482,25 +482,25 @@
 
 text\<open>If CertVerify is present then A has chosen PMS.\<close>
 lemma UseCertVerify_lemma:
-     "[| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \<in> parts (spies evs);
+     "[| Crypt (priK A) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>) \<in> parts (spies evs);
          evs \<in> tls;  A \<notin> bad |]
-      ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
+      ==> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs"
 apply (erule rev_mp)
 apply (erule tls.induct, force, simp_all, blast)
 done
 
 text\<open>Final version using the distributed KA instead of priK A\<close>
 lemma UseCertVerify:
-     "[| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|})
+     "[| Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>)
            \<in> parts (spies evs);
          certificate A KA \<in> parts (spies evs);
          evs \<in> tls;  A \<notin> bad |]
-      ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
+      ==> Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs"
 by (blast dest!: certificate_valid intro!: UseCertVerify_lemma)
 
 
 lemma no_Notes_A_PRF [simp]:
-     "evs \<in> tls ==> Notes A {|Agent B, Nonce (PRF x)|} \<notin> set evs"
+     "evs \<in> tls ==> Notes A \<lbrace>Agent B, Nonce (PRF x)\<rbrace> \<notin> set evs"
 apply (erule tls.induct, force, simp_all)
 txt\<open>ClientKeyExch: PMS is assumed to differ from any PRF.\<close>
 apply blast
@@ -538,15 +538,15 @@
 
 
 (** It is frustrating that we need two versions of the unicity results.
-    But Notes A {|Agent B, Nonce PMS|} determines both A and B.  Sometimes
+    But Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> determines both A and B.  Sometimes
     we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which
     determines B alone, and only if PMS is secret.
 **)
 
 text\<open>In A's internal Note, PMS determines A and B.\<close>
 lemma Notes_unique_PMS:
-     "[| Notes A  {|Agent B,  Nonce PMS|} \<in> set evs;
-         Notes A' {|Agent B', Nonce PMS|} \<in> set evs;
+     "[| Notes A  \<lbrace>Agent B,  Nonce PMS\<rbrace> \<in> set evs;
+         Notes A' \<lbrace>Agent B', Nonce PMS\<rbrace> \<in> set evs;
          evs \<in> tls |]
       ==> A=A' & B=B'"
 apply (erule rev_mp, erule rev_mp)
@@ -674,7 +674,7 @@
 
 text\<open>If A sends ClientKeyExch to an honest B, then the PMS will stay secret.\<close>
 lemma Spy_not_see_PMS:
-     "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
+     "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
          evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
       ==> Nonce PMS \<notin> analz (spies evs)"
 apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
@@ -696,7 +696,7 @@
 text\<open>If A sends ClientKeyExch to an honest B, then the MASTER SECRET
   will stay secret.\<close>
 lemma Spy_not_see_MS:
-     "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
+     "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
          evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
       ==> Nonce (PRF(PMS,NA,NB)) \<notin> analz (spies evs)"
 apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
@@ -720,7 +720,7 @@
   would send a message using a clientK generated from that PMS.\<close>
 lemma Says_clientK_unique:
      "[| Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
-         Notes A {|Agent B, Nonce PMS|} \<in> set evs;
+         Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
          evs \<in> tls;  A' \<noteq> Spy |]
       ==> A = A'"
 apply (erule rev_mp, erule rev_mp)
@@ -737,7 +737,7 @@
 text\<open>If A created PMS and has not leaked her clientK to the Spy,
   then it is completely secure: not even in parts!\<close>
 lemma clientK_not_spied:
-     "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
+     "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
          Says A Spy (Key (clientK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;
          evs \<in> tls |]
@@ -762,7 +762,7 @@
   send a message using a serverK generated from that PMS.\<close>
 lemma Says_serverK_unique:
      "[| Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs;
-         Notes A {|Agent B, Nonce PMS|} \<in> set evs;
+         Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
          evs \<in> tls;  A \<notin> bad;  B \<notin> bad;  B' \<noteq> Spy |]
       ==> B = B'"
 apply (erule rev_mp, erule rev_mp)
@@ -779,7 +779,7 @@
 text\<open>If A created PMS for B, and B has not leaked his serverK to the Spy,
   then it is completely secure: not even in parts!\<close>
 lemma serverK_not_spied:
-     "[| Notes A {|Agent B, Nonce PMS|} \<in> set evs;
+     "[| Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs;
          Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> tls |]
       ==> Key (serverK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)"
@@ -804,13 +804,13 @@
 text\<open>The mention of her name (A) in X assures A that B knows who she is.\<close>
 lemma TrustServerFinished [rule_format]:
      "[| X = Crypt (serverK(Na,Nb,M))
-               (Hash{|Number SID, Nonce M,
+               (Hash\<lbrace>Number SID, Nonce M,
                       Nonce Na, Number PA, Agent A,
-                      Nonce Nb, Number PB, Agent B|});
+                      Nonce Nb, Number PB, Agent B\<rbrace>);
          M = PRF(PMS,NA,NB);
          evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
       ==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs -->
-          Notes A {|Agent B, Nonce PMS|} \<in> set evs -->
+          Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs -->
           X \<in> parts (spies evs) --> Says B A X \<in> set evs"
 apply (erule ssubst)+
 apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
@@ -829,7 +829,7 @@
 lemma TrustServerMsg [rule_format]:
      "[| M = PRF(PMS,NA,NB);  evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
       ==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs -->
-          Notes A {|Agent B, Nonce PMS|} \<in> set evs -->
+          Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs -->
           Crypt (serverK(Na,Nb,M)) Y \<in> parts (spies evs)  -->
           (\<exists>A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) \<in> set evs)"
 apply (erule ssubst)
@@ -855,7 +855,7 @@
 lemma TrustClientMsg [rule_format]:
      "[| M = PRF(PMS,NA,NB);  evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
       ==> Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs -->
-          Notes A {|Agent B, Nonce PMS|} \<in> set evs -->
+          Notes A \<lbrace>Agent B, Nonce PMS\<rbrace> \<in> set evs -->
           Crypt (clientK(Na,Nb,M)) Y \<in> parts (spies evs) -->
           Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs"
 apply (erule ssubst)
@@ -878,7 +878,7 @@
          Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs;
          Says A' B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs;
          certificate A KA \<in> parts (spies evs);
-         Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))
+         Says A'' B (Crypt (invKey KA) (Hash\<lbrace>nb, Agent B, Nonce PMS\<rbrace>))
            \<in> set evs;
          evs \<in> tls;  A \<notin> bad;  B \<notin> bad |]
       ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs"
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/WooLam.thy
--- a/src/HOL/Auth/WooLam.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/WooLam.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -52,13 +52,13 @@
  | WL4:  "[| evs4 \<in> woolam;
              Says A'  B X         \<in> set evs4;
              Says A'' B (Agent A) \<in> set evs4 |]
-          ==> Says B Server {|Agent A, Agent B, X|} # evs4 \<in> woolam"
+          ==> Says B Server \<lbrace>Agent A, Agent B, X\<rbrace> # evs4 \<in> woolam"
 
          (*Server decrypts Alice's response for Bob.*)
  | WL5:  "[| evs5 \<in> woolam;
-             Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
+             Says B' Server \<lbrace>Agent A, Agent B, Crypt (shrK A) (Nonce NB)\<rbrace>
                \<in> set evs5 |]
-          ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
+          ==> Says Server B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>)
                  # evs5 \<in> woolam"
 
 
@@ -70,7 +70,7 @@
 
 (*A "possibility property": there are traces that reach the end*)
 lemma "\<exists>NB. \<exists>evs \<in> woolam.
-             Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \<in> set evs"
+             Says Server B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>) \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] woolam.Nil
                     [THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3,
@@ -113,7 +113,7 @@
   Alice, then she originated that certificate.  But we DO NOT know that B
   ever saw it: the Spy may have rerouted the message to the Server.*)
 lemma Server_trusts_WL4 [dest]:
-     "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
+     "[| Says B' Server \<lbrace>Agent A, Agent B, Crypt (shrK A) (Nonce NB)\<rbrace>
            \<in> set evs;
          A \<notin> bad;  evs \<in> woolam |]
       ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
@@ -124,17 +124,17 @@
 
 (*Server sent WL5 only if it received the right sort of message*)
 lemma Server_sent_WL5 [dest]:
-     "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs;
+     "[| Says Server B (Crypt (shrK B) \<lbrace>Agent A, NB\<rbrace>) \<in> set evs;
          evs \<in> woolam |]
-      ==> \<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
+      ==> \<exists>B'. Says B' Server \<lbrace>Agent A, Agent B, Crypt (shrK A) NB\<rbrace>
              \<in> set evs"
 by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
 
 (*If the encrypted message appears then it originated with the Server!*)
 lemma NB_Crypt_imp_Server_msg [rule_format]:
-     "[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
+     "[| Crypt (shrK B) \<lbrace>Agent A, NB\<rbrace> \<in> parts (spies evs);
          B \<notin> bad;  evs \<in> woolam |]
-      ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
+      ==> Says Server B (Crypt (shrK B) \<lbrace>Agent A, NB\<rbrace>) \<in> set evs"
 by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
 
 (*Guarantee for B.  If B gets the Server's certificate then A has encrypted
@@ -142,7 +142,7 @@
   But A may have sent the nonce to some other agent and it could have reached
   the Server via the Spy.*)
 lemma B_trusts_WL5:
-     "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs;
+     "[| Says S B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>): set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> woolam  |]
       ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
 by (blast dest!: NB_Crypt_imp_Server_msg)
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Yahalom.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -32,24 +32,24 @@
 
          (*Alice initiates a protocol run*)
  | YM1:  "[| evs1 \<in> yahalom;  Nonce NA \<notin> used evs1 |]
-          ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
+          ==> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom"
 
          (*Bob's response to Alice's message.*)
  | YM2:  "[| evs2 \<in> yahalom;  Nonce NB \<notin> used evs2;
-             Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
+             Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2 |]
           ==> Says B Server 
-                  {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+                  \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
                 # evs2 \<in> yahalom"
 
          (*The Server receives Bob's message.  He responds by sending a
             new session key to Alice, with a packet for forwarding to Bob.*)
  | YM3:  "[| evs3 \<in> yahalom;  Key KAB \<notin> used evs3;  KAB \<in> symKeys;
              Gets Server 
-                  {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+                  \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
                \<in> set evs3 |]
           ==> Says Server A
-                   {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
-                     Crypt (shrK B) {|Agent A, Key KAB|}|}
+                   \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA, Nonce NB\<rbrace>,
+                     Crypt (shrK B) \<lbrace>Agent A, Key KAB\<rbrace>\<rbrace>
                 # evs3 \<in> yahalom"
 
  | YM4:  
@@ -58,25 +58,25 @@
            @{term "A \<noteq> Server"} is needed for \<open>Says_Server_not_range\<close>.
            Alice can check that K is symmetric by its length.\<close>
          "[| evs4 \<in> yahalom;  A \<noteq> Server;  K \<in> symKeys;
-             Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|}
+             Gets A \<lbrace>Crypt(shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, X\<rbrace>
                 \<in> set evs4;
-             Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
-          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom"
+             Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4 |]
+          ==> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom"
 
          (*This message models possible leaks of session keys.  The Nonces
            identify the protocol run.  Quoting Server here ensures they are
            correct.*)
  | Oops: "[| evso \<in> yahalom;  
-             Says Server A {|Crypt (shrK A)
-                                   {|Agent B, Key K, Nonce NA, Nonce NB|},
-                             X|}  \<in> set evso |]
-          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> yahalom"
+             Says Server A \<lbrace>Crypt (shrK A)
+                                   \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>,
+                             X\<rbrace>  \<in> set evso |]
+          ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> yahalom"
 
 
 definition KeyWithNonce :: "[key, nat, event list] => bool" where
   "KeyWithNonce K NB evs ==
      \<exists>A B na X. 
-       Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} 
+       Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace>
          \<in> set evs"
 
 
@@ -88,7 +88,7 @@
 text\<open>A "possibility property": there are traces that reach the end\<close>
 lemma "[| A \<noteq> Server; K \<in> symKeys; Key K \<notin> used [] |]
       ==> \<exists>X NB. \<exists>evs \<in> yahalom.
-             Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+             Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] yahalom.Nil
                     [THEN yahalom.YM1, THEN yahalom.Reception,
@@ -116,7 +116,7 @@
 
 text\<open>Lets us treat YM4 using a similar argument as for the Fake case.\<close>
 lemma YM4_analz_knows_Spy:
-     "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs;  evs \<in> yahalom |]
+     "[| Gets A \<lbrace>Crypt (shrK A) Y, X\<rbrace> \<in> set evs;  evs \<in> yahalom |]
       ==> X \<in> analz (knows Spy evs)"
 by blast
 
@@ -125,7 +125,7 @@
 
 text\<open>For Oops\<close>
 lemma YM4_Key_parts_knows_Spy:
-     "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs
+     "Says Server A \<lbrace>Crypt (shrK A) \<lbrace>B,K,NA,NB\<rbrace>, X\<rbrace> \<in> set evs
       ==> K \<in> parts (knows Spy evs)"
   by (metis parts.Body parts.Fst parts.Snd  Says_imp_knows_Spy parts.Inj)
 
@@ -170,7 +170,7 @@
 text\<open>Describes the form of K when the Server sends this message.  Useful for
   Oops as well as main secrecy property.\<close>
 lemma Says_Server_not_range [simp]:
-     "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}
+     "[| Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace>
            \<in> set evs;   evs \<in> yahalom |]
       ==> K \<notin> range shrK"
 by (erule rev_mp, erule yahalom.induct, simp_all)
@@ -210,9 +210,9 @@
 text\<open>The Key K uniquely identifies the Server's  message.\<close>
 lemma unique_session_keys:
      "[| Says Server A
-          {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs;
+          \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> \<in> set evs;
         Says Server A'
-          {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs;
+          \<lbrace>Crypt (shrK A') \<lbrace>Agent B', Key K, na', nb'\<rbrace>, X'\<rbrace> \<in> set evs;
         evs \<in> yahalom |]
      ==> A=A' & B=B' & na=na' & nb=nb'"
 apply (erule rev_mp, erule rev_mp)
@@ -226,10 +226,10 @@
 lemma secrecy_lemma:
      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Says Server A
-            {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
-              Crypt (shrK B) {|Agent A, Key K|}|}
+            \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+              Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
            \<in> set evs -->
-          Notes Spy {|na, nb, Key K|} \<notin> set evs -->
+          Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs -->
           Key K \<notin> analz (knows Spy evs)"
 apply (erule yahalom.induct, force,
        drule_tac [6] YM4_analz_knows_Spy)
@@ -240,10 +240,10 @@
 text\<open>Final version\<close>
 lemma Spy_not_see_encrypted_key:
      "[| Says Server A
-            {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
-              Crypt (shrK B) {|Agent A, Key K|}|}
+            \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+              Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
            \<in> set evs;
-         Notes Spy {|na, nb, Key K|} \<notin> set evs;
+         Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Key K \<notin> analz (knows Spy evs)"
 by (blast dest: secrecy_lemma)
@@ -253,11 +253,11 @@
 
 text\<open>If the encrypted message appears then it originated with the Server\<close>
 lemma A_trusts_YM3:
-     "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
+     "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs);
          A \<notin> bad;  evs \<in> yahalom |]
        ==> Says Server A
-            {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
-              Crypt (shrK B) {|Agent A, Key K|}|}
+            \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+              Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
            \<in> set evs"
 apply (erule rev_mp)
 apply (erule yahalom.induct, force,
@@ -269,8 +269,8 @@
 text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with
   \<open>Spy_not_see_encrypted_key\<close>\<close>
 lemma A_gets_good_key:
-     "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
-         Notes Spy {|na, nb, Key K|} \<notin> set evs;
+     "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs);
+         Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Key K \<notin> analz (knows Spy evs)"
   by (metis A_trusts_YM3 secrecy_lemma)
@@ -281,12 +281,12 @@
 text\<open>B knows, by the first part of A's message, that the Server distributed
   the key for A and B.  But this part says nothing about nonces.\<close>
 lemma B_trusts_YM4_shrK:
-     "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs);
+     "[| Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs);
          B \<notin> bad;  evs \<in> yahalom |]
       ==> \<exists>NA NB. Says Server A
-                      {|Crypt (shrK A) {|Agent B, Key K,
-                                         Nonce NA, Nonce NB|},
-                        Crypt (shrK B) {|Agent A, Key K|}|}
+                      \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K,
+                                         Nonce NA, Nonce NB\<rbrace>,
+                        Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
                      \<in> set evs"
 apply (erule rev_mp)
 apply (erule yahalom.induct, force,
@@ -305,8 +305,8 @@
      "[|Crypt K (Nonce NB) \<in> parts (knows Spy evs);
         Nonce NB \<notin> analz (knows Spy evs);  evs \<in> yahalom|]
       ==> \<exists>A B NA. Says Server A
-                      {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
-                        Crypt (shrK B) {|Agent A, Key K|}|}
+                      \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>,
+                        Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
                      \<in> set evs"
 apply (erule rev_mp, erule rev_mp)
 apply (erule yahalom.induct, force,
@@ -329,14 +329,14 @@
 
 lemma KeyWithNonceI:
  "Says Server A
-          {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}
+          \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace>
         \<in> set evs ==> KeyWithNonce K NB evs"
 by (unfold KeyWithNonce_def, blast)
 
 lemma KeyWithNonce_Says [simp]:
    "KeyWithNonce K NB (Says S A X # evs) =
       (Server = S &
-       (\<exists>B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|})
+       (\<exists>B n X'. X = \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, n, Nonce NB\<rbrace>, X'\<rbrace>)
       | KeyWithNonce K NB evs)"
 by (simp add: KeyWithNonce_def, blast)
 
@@ -358,7 +358,7 @@
 text\<open>The Server message associates K with NB' and therefore not with any
   other nonce NB.\<close>
 lemma Says_Server_KeyWithNonce:
- "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|}
+ "[| Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB'\<rbrace>, X\<rbrace>
        \<in> set evs;
      NB \<noteq> NB';  evs \<in> yahalom |]
   ==> ~ KeyWithNonce K NB evs"
@@ -417,7 +417,7 @@
    for the induction to carry through.\<close>
 lemma single_Nonce_secrecy:
      "[| Says Server A
-          {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}
+          \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, na, Nonce NB'\<rbrace>, X\<rbrace>
          \<in> set evs;
          NB \<noteq> NB';  KAB \<notin> range shrK;  evs \<in> yahalom |]
       ==> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) =
@@ -430,8 +430,8 @@
 subsubsection\<open>The Nonce NB uniquely identifies B's message.\<close>
 
 lemma unique_NB:
-     "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
-         Crypt (shrK B') {|Agent A', Nonce NA', nb|} \<in> parts (knows Spy evs);
+     "[| Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs);
+         Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace> \<in> parts (knows Spy evs);
         evs \<in> yahalom;  B \<notin> bad;  B' \<notin> bad |]
       ==> NA' = NA & A' = A & B' = B"
 apply (erule rev_mp, erule rev_mp)
@@ -445,9 +445,9 @@
 text\<open>Variant useful for proving secrecy of NB.  Because nb is assumed to be
   secret, we no longer must assume B, B' not bad.\<close>
 lemma Says_unique_NB:
-     "[| Says C S   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+     "[| Says C S   \<lbrace>X,  Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
            \<in> set evs;
-         Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|}
+         Gets S' \<lbrace>X', Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace>\<rbrace>
            \<in> set evs;
          nb \<notin> analz (knows Spy evs);  evs \<in> yahalom |]
       ==> NA' = NA & A' = A & B' = B"
@@ -458,9 +458,9 @@
 subsubsection\<open>A nonce value is never used both as NA and as NB\<close>
 
 lemma no_nonce_YM1_YM2:
-     "[|Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \<in> parts(knows Spy evs);
+     "[|Crypt (shrK B') \<lbrace>Agent A', Nonce NB, nb'\<rbrace> \<in> parts(knows Spy evs);
         Nonce NB \<notin> analz (knows Spy evs);  evs \<in> yahalom|]
-  ==> Crypt (shrK B)  {|Agent A, na, Nonce NB|} \<notin> parts(knows Spy evs)"
+  ==> Crypt (shrK B)  \<lbrace>Agent A, na, Nonce NB\<rbrace> \<notin> parts(knows Spy evs)"
 apply (erule rev_mp, erule rev_mp)
 apply (erule yahalom.induct, force,
        frule_tac [6] YM4_parts_knows_Spy)
@@ -471,18 +471,18 @@
 
 text\<open>The Server sends YM3 only in response to YM2.\<close>
 lemma Says_Server_imp_YM2:
-     "[| Says Server A {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} \<in> set evs;
+     "[| Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, k, na, nb\<rbrace>, X\<rbrace> \<in> set evs;
          evs \<in> yahalom |]
-      ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |}
+      ==> Gets Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, na, nb\<rbrace>\<rbrace>
              \<in> set evs"
 by (erule rev_mp, erule yahalom.induct, auto)
 
 text\<open>A vital theorem for B, that nonce NB remains secure from the Spy.\<close>
 lemma Spy_not_see_NB :
      "[| Says B Server
-                {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+                \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
            \<in> set evs;
-         (\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
+         (\<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs);
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Nonce NB \<notin> analz (knows Spy evs)"
 apply (erule rev_mp, erule rev_mp)
@@ -521,17 +521,17 @@
   If this run is broken and the spy substitutes a certificate containing an
   old key, B has no means of telling.\<close>
 lemma B_trusts_YM4:
-     "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
-                  Crypt K (Nonce NB)|} \<in> set evs;
+     "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
+                  Crypt K (Nonce NB)\<rbrace> \<in> set evs;
          Says B Server
-           {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+           \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
            \<in> set evs;
-         \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
+         \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
        ==> Says Server A
-                   {|Crypt (shrK A) {|Agent B, Key K,
-                             Nonce NA, Nonce NB|},
-                     Crypt (shrK B) {|Agent A, Key K|}|}
+                   \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K,
+                             Nonce NA, Nonce NB\<rbrace>,
+                     Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
              \<in> set evs"
 by (blast dest: Spy_not_see_NB Says_unique_NB
                 Says_Server_imp_YM2 B_trusts_YM4_newK)
@@ -541,12 +541,12 @@
 text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with 
   \<open>Spy_not_see_encrypted_key\<close>\<close>
 lemma B_gets_good_key:
-     "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
-                  Crypt K (Nonce NB)|} \<in> set evs;
+     "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
+                  Crypt K (Nonce NB)\<rbrace> \<in> set evs;
          Says B Server
-           {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+           \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
            \<in> set evs;
-         \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
+         \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Key K \<notin> analz (knows Spy evs)"
   by (metis B_trusts_YM4 Spy_not_see_encrypted_key)
@@ -556,10 +556,10 @@
 
 text\<open>The encryption in message YM2 tells us it cannot be faked.\<close>
 lemma B_Said_YM2 [rule_format]:
-     "[|Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
+     "[|Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs);
         evs \<in> yahalom|]
       ==> B \<notin> bad -->
-          Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+          Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
             \<in> set evs"
 apply (erule rev_mp, erule yahalom.induct, force,
        frule_tac [6] YM4_parts_knows_Spy, simp_all)
@@ -569,10 +569,10 @@
 
 text\<open>If the server sends YM3 then B sent YM2\<close>
 lemma YM3_auth_B_to_A_lemma:
-     "[|Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
+     "[|Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace>
        \<in> set evs;  evs \<in> yahalom|]
       ==> B \<notin> bad -->
-          Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+          Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
             \<in> set evs"
 apply (erule rev_mp, erule yahalom.induct, simp_all)
 txt\<open>YM3, YM4\<close>
@@ -581,10 +581,10 @@
 
 text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close>
 lemma YM3_auth_B_to_A:
-     "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
+     "[| Gets A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace>
            \<in> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
-      ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+      ==> Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
        \<in> set evs"
   by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst
          not_parts_not_analz)
@@ -600,9 +600,9 @@
      "evs \<in> yahalom
       ==> Key K \<notin> analz (knows Spy evs) -->
           Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
-          Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) -->
+          Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs) -->
           B \<notin> bad -->
-          (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
+          (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)"
 apply (erule yahalom.induct, force,
        frule_tac [6] YM4_parts_knows_Spy)
 apply (analz_mono_contra, simp_all)
@@ -624,13 +624,13 @@
   Moreover, A associates K with NB (thus is talking about the same run).
   Other premises guarantee secrecy of K.\<close>
 lemma YM4_imp_A_Said_YM3 [rule_format]:
-     "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
-                  Crypt K (Nonce NB)|} \<in> set evs;
+     "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
+                  Crypt K (Nonce NB)\<rbrace> \<in> set evs;
          Says B Server
-           {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+           \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
            \<in> set evs;
-         (\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
+         (\<forall>NA k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs);
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
-      ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+      ==> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
 by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz)
 end
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Yahalom2.thy
--- a/src/HOL/Auth/Yahalom2.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Yahalom2.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -36,44 +36,44 @@
 
          (*Alice initiates a protocol run*)
  | YM1:  "[| evs1 \<in> yahalom;  Nonce NA \<notin> used evs1 |]
-          ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
+          ==> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom"
 
          (*Bob's response to Alice's message.*)
  | YM2:  "[| evs2 \<in> yahalom;  Nonce NB \<notin> used evs2;
-             Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
+             Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2 |]
           ==> Says B Server
-                  {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+                  \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
                 # evs2 \<in> yahalom"
 
          (*The Server receives Bob's message.  He responds by sending a
            new session key to Alice, with a certificate for forwarding to Bob.
            Both agents are quoted in the 2nd certificate to prevent attacks!*)
  | YM3:  "[| evs3 \<in> yahalom;  Key KAB \<notin> used evs3;
-             Gets Server {|Agent B, Nonce NB,
-                           Crypt (shrK B) {|Agent A, Nonce NA|}|}
+             Gets Server \<lbrace>Agent B, Nonce NB,
+                           Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
                \<in> set evs3 |]
           ==> Says Server A
-               {|Nonce NB,
-                 Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
-                 Crypt (shrK B) {|Agent A, Agent B, Key KAB, Nonce NB|}|}
+               \<lbrace>Nonce NB,
+                 Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA\<rbrace>,
+                 Crypt (shrK B) \<lbrace>Agent A, Agent B, Key KAB, Nonce NB\<rbrace>\<rbrace>
                  # evs3 \<in> yahalom"
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.*)
  | YM4:  "[| evs4 \<in> yahalom;
-             Gets A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
-                      X|}  \<in> set evs4;
-             Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
-          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom"
+             Gets A \<lbrace>Nonce NB, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>,
+                      X\<rbrace>  \<in> set evs4;
+             Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4 |]
+          ==> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom"
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.  Quoting Server here ensures they are
            correct. *)
  | Oops: "[| evso \<in> yahalom;
-             Says Server A {|Nonce NB,
-                             Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
-                             X|}  \<in> set evso |]
-          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> yahalom"
+             Says Server A \<lbrace>Nonce NB,
+                             Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>,
+                             X\<rbrace>  \<in> set evso |]
+          ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> yahalom"
 
 
 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
@@ -84,7 +84,7 @@
 text\<open>A "possibility property": there are traces that reach the end\<close>
 lemma "Key K \<notin> used []
        ==> \<exists>X NB. \<exists>evs \<in> yahalom.
-             Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+             Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] yahalom.Nil
                     [THEN yahalom.YM1, THEN yahalom.Reception,
@@ -111,7 +111,7 @@
 text\<open>Result for reasoning about the encrypted portion of messages.
 Lets us treat YM4 using a similar argument as for the Fake case.\<close>
 lemma YM4_analz_knows_Spy:
-     "[| Gets A {|NB, Crypt (shrK A) Y, X|} \<in> set evs;  evs \<in> yahalom |]
+     "[| Gets A \<lbrace>NB, Crypt (shrK A) Y, X\<rbrace> \<in> set evs;  evs \<in> yahalom |]
       ==> X \<in> analz (knows Spy evs)"
 by blast
 
@@ -157,7 +157,7 @@
 text\<open>Describes the form of K when the Server sends this message.  Useful for
   Oops as well as main secrecy property.\<close>
 lemma Says_Server_message_form:
-     "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|}
+     "[| Says Server A \<lbrace>nb', Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, X\<rbrace>
           \<in> set evs;  evs \<in> yahalom |]
       ==> K \<notin> range shrK"
 by (erule rev_mp, erule yahalom.induct, simp_all)
@@ -194,9 +194,9 @@
 text\<open>The Key K uniquely identifies the Server's  message\<close>
 lemma unique_session_keys:
      "[| Says Server A
-          {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \<in> set evs;
+          \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, X\<rbrace> \<in> set evs;
         Says Server A'
-          {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \<in> set evs;
+          \<lbrace>nb', Crypt (shrK A') \<lbrace>Agent B', Key K, na'\<rbrace>, X'\<rbrace> \<in> set evs;
         evs \<in> yahalom |]
      ==> A=A' & B=B' & na=na' & nb=nb'"
 apply (erule rev_mp, erule rev_mp)
@@ -211,10 +211,10 @@
 lemma secrecy_lemma:
      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Says Server A
-            {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
-                  Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
+            \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>,
+                  Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace>
            \<in> set evs -->
-          Notes Spy {|na, nb, Key K|} \<notin> set evs -->
+          Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs -->
           Key K \<notin> analz (knows Spy evs)"
 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
        drule_tac [6] YM4_analz_knows_Spy)
@@ -226,10 +226,10 @@
 text\<open>Final version\<close>
 lemma Spy_not_see_encrypted_key:
      "[| Says Server A
-            {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
-                  Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
+            \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>,
+                  Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace>
          \<in> set evs;
-         Notes Spy {|na, nb, Key K|} \<notin> set evs;
+         Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Key K \<notin> analz (knows Spy evs)"
 by (blast dest: secrecy_lemma Says_Server_message_form)
@@ -245,10 +245,10 @@
 @{term "Key K \<notin> analz (knows Spy evs)"}.\<close>
 lemma Spy_not_know_encrypted_key:
      "[| Says Server A
-            {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
-                  Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
+            \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>,
+                  Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace>
          \<in> set evs;
-         Notes Spy {|na, nb, Key K|} \<notin> set evs;
+         Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Key K \<notin> knows Spy evs"
 by (blast dest: Spy_not_see_encrypted_key)
@@ -259,11 +259,11 @@
 text\<open>If the encrypted message appears then it originated with the Server.
   May now apply \<open>Spy_not_see_encrypted_key\<close>, subject to its conditions.\<close>
 lemma A_trusts_YM3:
-     "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
+     "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> parts (knows Spy evs);
          A \<notin> bad;  evs \<in> yahalom |]
       ==> \<exists>nb. Says Server A
-                    {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
-                          Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
+                    \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>,
+                          Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace>
                   \<in> set evs"
 apply (erule rev_mp)
 apply (erule yahalom.induct, force,
@@ -275,8 +275,8 @@
 text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with 
 \<open>Spy_not_see_encrypted_key\<close>\<close>
 theorem A_gets_good_key:
-     "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
-         \<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs;
+     "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> parts (knows Spy evs);
+         \<forall>nb. Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Key K \<notin> analz (knows Spy evs)"
 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
@@ -287,13 +287,13 @@
 text\<open>B knows, by the first part of A's message, that the Server distributed
   the key for A and B, and has associated it with NB.\<close>
 lemma B_trusts_YM4_shrK:
-     "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
+     "[| Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>
            \<in> parts (knows Spy evs);
          B \<notin> bad;  evs \<in> yahalom |]
   ==> \<exists>NA. Says Server A
-             {|Nonce NB,
-               Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
-               Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
+             \<lbrace>Nonce NB,
+               Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>,
+               Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>\<rbrace>
              \<in> set evs"
 apply (erule rev_mp)
 apply (erule yahalom.induct, force,
@@ -309,13 +309,13 @@
 text\<open>What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   because we do not have to show that NB is secret.\<close>
 lemma B_trusts_YM4:
-     "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},  X|}
+     "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>,  X\<rbrace>
            \<in> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   ==> \<exists>NA. Says Server A
-             {|Nonce NB,
-               Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
-               Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
+             \<lbrace>Nonce NB,
+               Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>,
+               Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>\<rbrace>
             \<in> set evs"
 by (blast dest!: B_trusts_YM4_shrK)
 
@@ -323,9 +323,9 @@
 text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with 
 \<open>Spy_not_see_encrypted_key\<close>\<close>
 theorem B_gets_good_key:
-     "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
+     "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>, X\<rbrace>
            \<in> set evs;
-         \<forall>na. Notes Spy {|na, Nonce NB, Key K|} \<notin> set evs;
+         \<forall>na. Notes Spy \<lbrace>na, Nonce NB, Key K\<rbrace> \<notin> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Key K \<notin> analz (knows Spy evs)"
 by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
@@ -335,10 +335,10 @@
 
 text\<open>The encryption in message YM2 tells us it cannot be faked.\<close>
 lemma B_Said_YM2:
-     "[| Crypt (shrK B) {|Agent A, Nonce NA|} \<in> parts (knows Spy evs);
+     "[| Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace> \<in> parts (knows Spy evs);
          B \<notin> bad;  evs \<in> yahalom |]
-      ==> \<exists>NB. Says B Server {|Agent B, Nonce NB,
-                               Crypt (shrK B) {|Agent A, Nonce NA|}|}
+      ==> \<exists>NB. Says B Server \<lbrace>Agent B, Nonce NB,
+                               Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
                       \<in> set evs"
 apply (erule rev_mp)
 apply (erule yahalom.induct, force,
@@ -350,11 +350,11 @@
 
 text\<open>If the server sends YM3 then B sent YM2, perhaps with a different NB\<close>
 lemma YM3_auth_B_to_A_lemma:
-     "[| Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
+     "[| Says Server A \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, X\<rbrace>
            \<in> set evs;
          B \<notin> bad;  evs \<in> yahalom |]
-      ==> \<exists>nb'. Says B Server {|Agent B, nb',
-                                   Crypt (shrK B) {|Agent A, Nonce NA|}|}
+      ==> \<exists>nb'. Says B Server \<lbrace>Agent B, nb',
+                                   Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
                        \<in> set evs"
 apply (erule rev_mp)
 apply (erule yahalom.induct, simp_all)
@@ -364,11 +364,11 @@
 
 text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close>
 theorem YM3_auth_B_to_A:
-     "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
+     "[| Gets A \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, X\<rbrace>
            \<in> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
  ==> \<exists>nb'. Says B Server
-                  {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|}
+                  \<lbrace>Agent B, nb', Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
                \<in> set evs"
 by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma)
 
@@ -385,8 +385,8 @@
 text\<open>This lemma allows a use of \<open>unique_session_keys\<close> in the next proof,
   which otherwise is extremely slow.\<close>
 lemma secure_unique_session_keys:
-     "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> analz (spies evs);
-         Crypt (shrK A') {|Agent B', Key K, na'|} \<in> analz (spies evs);
+     "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> analz (spies evs);
+         Crypt (shrK A') \<lbrace>Agent B', Key K, na'\<rbrace> \<in> analz (spies evs);
          Key K \<notin> analz (knows Spy evs);  evs \<in> yahalom |]
      ==> A=A' & B=B'"
 by (blast dest!: A_trusts_YM3 dest: unique_session_keys Crypt_Spy_analz_bad)
@@ -397,10 +397,10 @@
       ==> Key K \<notin> analz (knows Spy evs) -->
           K \<in> symKeys -->
           Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
-          Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
+          Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>
             \<in> parts (knows Spy evs) -->
           B \<notin> bad -->
-          (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
+          (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)"
 apply (erule yahalom.induct, force,
        frule_tac [6] YM4_parts_knows_Spy)
 apply (analz_mono_contra, simp_all)
@@ -419,11 +419,11 @@
   Moreover, A associates K with NB (thus is talking about the same run).
   Other premises guarantee secrecy of K.\<close>
 theorem YM4_imp_A_Said_YM3 [rule_format]:
-     "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},
-                  Crypt K (Nonce NB)|} \<in> set evs;
-         (\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs);
+     "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>,
+                  Crypt K (Nonce NB)\<rbrace> \<in> set evs;
+         (\<forall>NA. Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> \<notin> set evs);
          K \<in> symKeys;  A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
-      ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+      ==> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
 by (blast intro: Auth_A_to_B_lemma
           dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK)
 
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Yahalom_Bad.thy
--- a/src/HOL/Auth/Yahalom_Bad.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Yahalom_Bad.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -31,34 +31,34 @@
 
          (*Alice initiates a protocol run*)
  | YM1:  "[| evs1 \<in> yahalom;  Nonce NA \<notin> used evs1 |]
-          ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
+          ==> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom"
 
          (*Bob's response to Alice's message.*)
  | YM2:  "[| evs2 \<in> yahalom;  Nonce NB \<notin> used evs2;
-             Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
+             Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2 |]
           ==> Says B Server
-                  {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+                  \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
                 # evs2 \<in> yahalom"
 
          (*The Server receives Bob's message.  He responds by sending a
             new session key to Alice, with a packet for forwarding to Bob.*)
  | YM3:  "[| evs3 \<in> yahalom;  Key KAB \<notin> used evs3;  KAB \<in> symKeys;
              Gets Server
-                  {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+                  \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
                \<in> set evs3 |]
           ==> Says Server A
-                   {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
-                     Crypt (shrK B) {|Agent A, Key KAB|}|}
+                   \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA, Nonce NB\<rbrace>,
+                     Crypt (shrK B) \<lbrace>Agent A, Key KAB\<rbrace>\<rbrace>
                 # evs3 \<in> yahalom"
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.  The premise
            A \<noteq> Server is needed to prove Says_Server_not_range.*)
  | YM4:  "[| evs4 \<in> yahalom;  A \<noteq> Server;  K \<in> symKeys;
-             Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|}
+             Gets A \<lbrace>Crypt(shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, X\<rbrace>
                 \<in> set evs4;
-             Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
-          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom"
+             Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4 |]
+          ==> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom"
 
 
 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
@@ -70,7 +70,7 @@
 text\<open>A "possibility property": there are traces that reach the end\<close>
 lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |] 
        ==> \<exists>X NB. \<exists>evs \<in> yahalom.
-              Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+              Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] yahalom.Nil
                     [THEN yahalom.YM1, THEN yahalom.Reception,
@@ -98,7 +98,7 @@
 
 text\<open>Lets us treat YM4 using a similar argument as for the Fake case.\<close>
 lemma YM4_analz_knows_Spy:
-     "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs;  evs \<in> yahalom |]
+     "[| Gets A \<lbrace>Crypt (shrK A) Y, X\<rbrace> \<in> set evs;  evs \<in> yahalom |]
       ==> X \<in> analz (knows Spy evs)"
 by blast
 
@@ -168,9 +168,9 @@
 text\<open>The Key K uniquely identifies the Server's  message.\<close>
 lemma unique_session_keys:
      "[| Says Server A
-          {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs;
+          \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> \<in> set evs;
         Says Server A'
-          {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs;
+          \<lbrace>Crypt (shrK A') \<lbrace>Agent B', Key K, na', nb'\<rbrace>, X'\<rbrace> \<in> set evs;
         evs \<in> yahalom |]
      ==> A=A' & B=B' & na=na' & nb=nb'"
 apply (erule rev_mp, erule rev_mp)
@@ -184,8 +184,8 @@
 lemma secrecy_lemma:
      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Says Server A
-            {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
-              Crypt (shrK B) {|Agent A, Key K|}|}
+            \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+              Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
            \<in> set evs -->
           Key K \<notin> analz (knows Spy evs)"
 apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy)
@@ -196,8 +196,8 @@
 text\<open>Final version\<close>
 lemma Spy_not_see_encrypted_key:
      "[| Says Server A
-            {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
-              Crypt (shrK B) {|Agent A, Key K|}|}
+            \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+              Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
            \<in> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Key K \<notin> analz (knows Spy evs)"
@@ -208,11 +208,11 @@
 
 text\<open>If the encrypted message appears then it originated with the Server\<close>
 lemma A_trusts_YM3:
-     "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
+     "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs);
          A \<notin> bad;  evs \<in> yahalom |]
        ==> Says Server A
-            {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
-              Crypt (shrK B) {|Agent A, Key K|}|}
+            \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+              Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
            \<in> set evs"
 apply (erule rev_mp)
 apply (erule yahalom.induct, force,
@@ -224,7 +224,7 @@
 text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with
   \<open>Spy_not_see_encrypted_key\<close>\<close>
 lemma A_gets_good_key:
-     "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
+     "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs);
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Key K \<notin> analz (knows Spy evs)"
 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
@@ -234,11 +234,11 @@
 text\<open>B knows, by the first part of A's message, that the Server distributed
   the key for A and B.  But this part says nothing about nonces.\<close>
 lemma B_trusts_YM4_shrK:
-     "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs);
+     "[| Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs);
          B \<notin> bad;  evs \<in> yahalom |]
       ==> \<exists>NA NB. Says Server A
-                      {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
-                        Crypt (shrK B) {|Agent A, Key K|}|}
+                      \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>,
+                        Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
                      \<in> set evs"
 apply (erule rev_mp)
 apply (erule yahalom.induct, force,
@@ -262,9 +262,9 @@
      "[|Key K \<notin> analz (knows Spy evs);  evs \<in> yahalom|]
       ==> Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
           (\<exists>A B NA. Says Server A
-                      {|Crypt (shrK A) {|Agent B, Key K,
-                                Nonce NA, Nonce NB|},
-                        Crypt (shrK B) {|Agent A, Key K|}|}
+                      \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K,
+                                Nonce NA, Nonce NB\<rbrace>,
+                        Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
                      \<in> set evs)"
 apply (erule rev_mp)
 apply (erule yahalom.induct, force,
@@ -285,15 +285,15 @@
 text\<open>B's session key guarantee from YM4.  The two certificates contribute to a
   single conclusion about the Server's message.\<close>
 lemma B_trusts_YM4:
-     "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
-                  Crypt K (Nonce NB)|} \<in> set evs;
+     "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
+                  Crypt K (Nonce NB)\<rbrace> \<in> set evs;
          Says B Server
-           {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+           \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
            \<in> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
        ==> \<exists>na nb. Says Server A
-                   {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
-                     Crypt (shrK B) {|Agent A, Key K|}|}
+                   \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
+                     Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
              \<in> set evs"
 by (blast dest: B_trusts_YM4_newK B_trusts_YM4_shrK Spy_not_see_encrypted_key
                 unique_session_keys)
@@ -302,10 +302,10 @@
 text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with 
   \<open>Spy_not_see_encrypted_key\<close>\<close>
 lemma B_gets_good_key:
-     "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
-                  Crypt K (Nonce NB)|} \<in> set evs;
+     "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
+                  Crypt K (Nonce NB)\<rbrace> \<in> set evs;
          Says B Server
-           {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+           \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
            \<in> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
       ==> Key K \<notin> analz (knows Spy evs)"
@@ -325,9 +325,9 @@
      "evs \<in> yahalom
       ==> Key K \<notin> analz (knows Spy evs) -->
           Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
-          Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) -->
+          Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs) -->
           B \<notin> bad -->
-          (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
+          (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)"
 apply (erule yahalom.induct, force,
        frule_tac [6] YM4_parts_knows_Spy)
 apply (analz_mono_contra, simp_all)
@@ -349,13 +349,13 @@
   Moreover, A associates K with NB (thus is talking about the same run).
   Other premises guarantee secrecy of K.\<close>
 lemma YM4_imp_A_Said_YM3 [rule_format]:
-     "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
-                  Crypt K (Nonce NB)|} \<in> set evs;
+     "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
+                  Crypt K (Nonce NB)\<rbrace> \<in> set evs;
          Says B Server
-           {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+           \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace>
            \<in> set evs;
          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
-      ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+      ==> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
 by (blast intro!: A_Said_YM3_lemma
           dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
 
diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/ZhouGollmann.thy
--- a/src/HOL/Auth/ZhouGollmann.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/ZhouGollmann.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -43,24 +43,24 @@
     rather than to keep M secret.*)
 | ZG1: "[| evs1 \<in> zg;  Nonce L \<notin> used evs1; C = Crypt K (Number m);
            K \<in> symKeys;
-           NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|]
-       ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} # evs1 \<in> zg"
+           NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>|]
+       ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> # evs1 \<in> zg"
 
   (*B must check that NRO is A's signature to learn the sender's name*)
 | ZG2: "[| evs2 \<in> zg;
-           Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs2;
-           NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
-           NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|]
-       ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} # evs2  \<in>  zg"
+           Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs2;
+           NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
+           NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>|]
+       ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> # evs2  \<in>  zg"
 
   (*A must check that NRR is B's signature to learn the sender's name;
     without spy, the matching label would be enough*)
 | ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys;
-           Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3;
-           Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3;
-           NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
-           sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}|]
-       ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
+           Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs3;
+           Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs3;
+           NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
+           sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>|]
+       ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace>
              # evs3 \<in> zg"
 
  (*TTP checks that sub_K is A's signature to learn who issued K, then
@@ -70,14 +70,14 @@
    also allowing lemma @{text Crypt_used_imp_spies} to omit the condition
    @{term "K \<noteq> priK TTP"}. *)
 | ZG4: "[| evs4 \<in> zg; K \<in> symKeys;
-           Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
+           Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace>
              \<in> set evs4;
-           sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
-           con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
-                                      Nonce L, Key K|}|]
+           sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
+           con_K = Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B,
+                                      Nonce L, Key K\<rbrace>|]
        ==> Says TTP Spy con_K
            #
-           Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+           Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
            # evs4 \<in> zg"
 
 
@@ -92,8 +92,8 @@
 text\<open>A "possibility property": there are traces that reach the end\<close>
 lemma "[|A \<noteq> B; TTP \<noteq> A; TTP \<noteq> B; K \<in> symKeys|] ==>
      \<exists>L. \<exists>evs \<in> zg.
-           Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K,
-               Crypt (priK TTP) {|Number f_con, Agent A, Agent B, Nonce L, Key K|} |}
+           Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K,
+               Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>\<rbrace>
                \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] zg.Nil
@@ -128,18 +128,18 @@
 done
 
 lemma Notes_TTP_imp_Gets:
-     "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K |}
+     "[|Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
            \<in> set evs;
-        sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+        sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
         evs \<in> zg|]
-    ==> Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+    ==> Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
 apply (erule rev_mp)
 apply (erule zg.induct, auto)
 done
 
 text\<open>For reasoning about C, which is encrypted in message ZG2\<close>
 lemma ZG2_msg_in_parts_spies:
-     "[|Gets B {|F, B', L, C, X|} \<in> set evs; evs \<in> zg|]
+     "[|Gets B \<lbrace>F, B', L, C, X\<rbrace> \<in> set evs; evs \<in> zg|]
       ==> C \<in> parts (spies evs)"
 by (blast dest: Gets_imp_Says)
 
@@ -165,10 +165,10 @@
 
 text\<open>Strong conclusion for a good agent\<close>
 lemma NRO_validity_good:
-     "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+     "[|NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
         NRO \<in> parts (spies evs);
         A \<notin> bad;  evs \<in> zg |]
-     ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+     ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs"
 apply clarify
 apply (erule rev_mp)
 apply (erule zg.induct)
@@ -176,7 +176,7 @@
 done
 
 lemma NRO_sender:
-     "[|Says A' B {|n, b, l, C, Crypt (priK A) X|} \<in> set evs; evs \<in> zg|]
+     "[|Says A' B \<lbrace>n, b, l, C, Crypt (priK A) X\<rbrace> \<in> set evs; evs \<in> zg|]
     ==> A' \<in> {A,Spy}"
 apply (erule rev_mp)  
 apply (erule zg.induct, simp_all)
@@ -184,10 +184,10 @@
 
 text\<open>Holds also for @{term "A = Spy"}!\<close>
 theorem NRO_validity:
-     "[|Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
-        NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+     "[|Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs;
+        NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
         A \<notin> broken;  evs \<in> zg |]
-     ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+     ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs"
 apply (drule Gets_imp_Says, assumption) 
 apply clarify 
 apply (frule NRO_sender, auto)
@@ -205,10 +205,10 @@
 
 text\<open>Strong conclusion for a good agent\<close>
 lemma NRR_validity_good:
-     "[|NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+     "[|NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
         NRR \<in> parts (spies evs);
         B \<notin> bad;  evs \<in> zg |]
-     ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+     ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs"
 apply clarify
 apply (erule rev_mp)
 apply (erule zg.induct) 
@@ -216,7 +216,7 @@
 done
 
 lemma NRR_sender:
-     "[|Says B' A {|n, a, l, Crypt (priK B) X|} \<in> set evs; evs \<in> zg|]
+     "[|Says B' A \<lbrace>n, a, l, Crypt (priK B) X\<rbrace> \<in> set evs; evs \<in> zg|]
     ==> B' \<in> {B,Spy}"
 apply (erule rev_mp)  
 apply (erule zg.induct, simp_all)
@@ -224,10 +224,10 @@
 
 text\<open>Holds also for @{term "B = Spy"}!\<close>
 theorem NRR_validity:
-     "[|Says B' A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs;
-        NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+     "[|Says B' A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs;
+        NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
         B \<notin> broken; evs \<in> zg|]
-    ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+    ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs"
 apply clarify 
 apply (frule NRR_sender, auto)
 txt\<open>We are left with the case where @{term "B' = Spy"} and  @{term "B' \<noteq> B"},
@@ -243,10 +243,10 @@
 
 text\<open>Strong conclusion for a good agent\<close>
 lemma sub_K_validity_good:
-     "[|sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+     "[|sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
         sub_K \<in> parts (spies evs);
         A \<notin> bad;  evs \<in> zg |]
-     ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+     ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
 apply clarify
 apply (erule rev_mp)
 apply (erule zg.induct)
@@ -256,7 +256,7 @@
 done
 
 lemma sub_K_sender:
-     "[|Says A' TTP {|n, b, l, k, Crypt (priK A) X|} \<in> set evs;  evs \<in> zg|]
+     "[|Says A' TTP \<lbrace>n, b, l, k, Crypt (priK A) X\<rbrace> \<in> set evs;  evs \<in> zg|]
     ==> A' \<in> {A,Spy}"
 apply (erule rev_mp)  
 apply (erule zg.induct, simp_all)
@@ -264,10 +264,10 @@
 
 text\<open>Holds also for @{term "A = Spy"}!\<close>
 theorem sub_K_validity:
-     "[|Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
-        sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+     "[|Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs;
+        sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
         A \<notin> broken;  evs \<in> zg |]
-     ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+     ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
 apply (drule Gets_imp_Says, assumption) 
 apply clarify 
 apply (frule sub_K_sender, auto)
@@ -288,9 +288,9 @@
 lemma con_K_validity:
      "[|con_K \<in> used evs;
         con_K = Crypt (priK TTP)
-                  {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
+                  \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>;
         evs \<in> zg |]
-    ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+    ==> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
           \<in> set evs"
 apply clarify
 apply (erule rev_mp)
@@ -306,11 +306,11 @@
  @{term sub_K}.  We assume that @{term A} is not broken.  Importantly, nothing
   needs to be assumed about the form of @{term con_K}!\<close>
 lemma Notes_TTP_imp_Says_A:
-     "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+     "[|Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
            \<in> set evs;
-        sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+        sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
         A \<notin> broken; evs \<in> zg|]
-     ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+     ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
 apply clarify
 apply (erule rev_mp)
 apply (erule zg.induct)
@@ -324,11 +324,11 @@
    assume that @{term A} is not broken.\<close>
 theorem B_sub_K_validity:
      "[|con_K \<in> used evs;
-        con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
-                                   Nonce L, Key K|};
-        sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+        con_K = Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B,
+                                   Nonce L, Key K\<rbrace>;
+        sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
         A \<notin> broken; evs \<in> zg|]
-     ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+     ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
 by (blast dest: con_K_validity Notes_TTP_imp_Says_A)
 
 
@@ -340,9 +340,9 @@
 
 text\<open>Strange: unicity of the label protects @{term A}?\<close>
 lemma A_unicity: 
-     "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
+     "[|NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
         NRO \<in> parts (spies evs);
-        Says A B {|Number f_nro, Agent B, Nonce L, Crypt K M', NRO'|}
+        Says A B \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M', NRO'\<rbrace>
           \<in> set evs;
         A \<notin> bad; evs \<in> zg |]
      ==> M'=M"
@@ -359,13 +359,13 @@
 text\<open>Fairness lemma: if @{term sub_K} exists, then @{term A} holds 
 NRR.  Relies on unicity of labels.\<close>
 lemma sub_K_implies_NRR:
-     "[| NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
-         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
+     "[| NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
+         NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, Crypt K M\<rbrace>;
          sub_K \<in> parts (spies evs);
          NRO \<in> parts (spies evs);
-         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+         sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
          A \<notin> bad;  evs \<in> zg |]
-     ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+     ==> Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs"
 apply clarify
 apply hypsubst_thin
 apply (erule rev_mp)
@@ -382,7 +382,7 @@
 
 
 lemma Crypt_used_imp_L_used:
-     "[| Crypt (priK TTP) {|F, A, B, L, K|} \<in> used evs; evs \<in> zg |]
+     "[| Crypt (priK TTP) \<lbrace>F, A, B, L, K\<rbrace> \<in> used evs; evs \<in> zg |]
       ==> L \<in> used evs"
 apply (erule rev_mp)
 apply (erule zg.induct, auto)
@@ -400,11 +400,11 @@
      "[|con_K \<in> used evs;
         NRO \<in> parts (spies evs);
         con_K = Crypt (priK TTP)
-                      {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
-        NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
-        NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
+                      \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>;
+        NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
+        NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, Crypt K M\<rbrace>;
         A \<notin> bad;  evs \<in> zg |]
-    ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+    ==> Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs"
 apply clarify
 apply (erule rev_mp)
 apply (erule rev_mp)
@@ -427,10 +427,10 @@
 A}.\<close>
 theorem B_fairness_NRR:
      "[|NRR \<in> used evs;
-        NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
-        NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+        NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
+        NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
         B \<notin> bad; evs \<in> zg |]
-    ==> Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+    ==> Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs"
 apply clarify
 apply (erule rev_mp)
 apply (erule zg.induct)
diff -r e96292f32c3c -r 38b73f7940af src/HOL/UNITY/Simple/NSP_Bad.thy
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -33,7 +33,7 @@
   NS1 :: "(state*state) set"
   where "NS1 = {(s1,s').
              \<exists>A1 B NA.
-                 s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
+                 s' = Says A1 B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A1\<rbrace>) # s1
                & Nonce NA \<notin> used s1}"
 
   (*Bob responds to Alice's message with a further nonce*)
@@ -41,8 +41,8 @@
   NS2 :: "(state*state) set"
   where "NS2 = {(s2,s').
              \<exists>A' A2 B NA NB.
-                 s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2
-               & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) \<in> set s2
+                 s' = Says B A2 (Crypt (pubK A2) \<lbrace>Nonce NA, Nonce NB\<rbrace>) # s2
+               & Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A2\<rbrace>) \<in> set s2
                & Nonce NB \<notin> used s2}"
 
   (*Alice proves her existence by sending NB back to Bob.*)
@@ -51,8 +51,8 @@
   where "NS3 = {(s3,s').
              \<exists>A3 B' B NA NB.
                  s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3
-               & Says A3  B (Crypt (pubK B) {|Nonce NA, Agent A3|}) \<in> set s3
-               & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) \<in> set s3}"
+               & Says A3  B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A3\<rbrace>) \<in> set s3
+               & Says B' A3 (Crypt (pubK A3) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s3}"
 
 
 definition Nprg :: "state program" where
@@ -151,8 +151,8 @@
      nonce is secret.  (Honest users generate fresh nonces.)*}
 lemma no_nonce_NS1_NS2:
  "Nprg
-  \<in> Always {s. Crypt (pubK C) {|NA', Nonce NA|} \<in> parts (spies s) -->
-                Crypt (pubK B) {|Nonce NA, Agent A|} \<in> parts (spies s) -->
+  \<in> Always {s. Crypt (pubK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies s) -->
+                Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies s) -->
                 Nonce NA \<in> analz (spies s)}"
 apply ns_induct
 apply (blast intro: analz_insertI)+
@@ -167,8 +167,8 @@
 lemma unique_NA_lemma:
      "Nprg
   \<in> Always {s. Nonce NA \<notin> analz (spies s) -->
-                Crypt(pubK B) {|Nonce NA, Agent A|} \<in> parts(spies s) -->
-                Crypt(pubK B') {|Nonce NA, Agent A'|} \<in> parts(spies s) -->
+                Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts(spies s) -->
+                Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies s) -->
                 A=A' & B=B'}"
 apply ns_induct
 apply auto
@@ -177,8 +177,8 @@
 
 text{*Unicity for NS1: nonce NA identifies agents A and B*}
 lemma unique_NA:
-     "[| Crypt(pubK B)  {|Nonce NA, Agent A|} \<in> parts(spies s);
-         Crypt(pubK B') {|Nonce NA, Agent A'|} \<in> parts(spies s);
+     "[| Crypt(pubK B)  \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts(spies s);
+         Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies s);
          Nonce NA \<notin> analz (spies s);
          s \<in> reachable Nprg |]
       ==> A=A' & B=B'"
@@ -189,7 +189,7 @@
 lemma Spy_not_see_NA:
      "[| A \<notin> bad;  B \<notin> bad |]
   ==> Nprg \<in> Always
-              {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) \<in> set s
+              {s. Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s
                   --> Nonce NA \<notin> analz (spies s)}"
 apply ns_induct
 txt{*NS3*}
@@ -208,9 +208,9 @@
 lemma A_trusts_NS2:
  "[| A \<notin> bad;  B \<notin> bad |]
   ==> Nprg \<in> Always
-              {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) \<in> set s &
-                  Crypt(pubK A) {|Nonce NA, Nonce NB|} \<in> parts (knows Spy s)
-         --> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}) \<in> set s}"
+              {s. Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s &
+                  Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (knows Spy s)
+         --> Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s}"
   (*insert an invariant for use in some of the subgoals*)
 apply (insert Spy_not_see_NA [of A B NA], simp, ns_induct)
 apply (auto dest: unique_NA)
@@ -221,8 +221,8 @@
 lemma B_trusts_NS1:
      "Nprg \<in> Always
               {s. Nonce NA \<notin> analz (spies s) -->
-                  Crypt (pubK B) {|Nonce NA, Agent A|} \<in> parts (spies s)
-         --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) \<in> set s}"
+                  Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies s)
+         --> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s}"
 apply ns_induct
 apply blast
 done
@@ -235,8 +235,8 @@
 lemma unique_NB_lemma:
  "Nprg
   \<in> Always {s. Nonce NB \<notin> analz (spies s)  -->
-                Crypt (pubK A) {|Nonce NA, Nonce NB|} \<in> parts (spies s) -->
-                Crypt(pubK A'){|Nonce NA', Nonce NB|} \<in> parts(spies s) -->
+                Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies s) -->
+                Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies s) -->
                 A=A' & NA=NA'}"
 apply ns_induct
 apply auto
@@ -244,8 +244,8 @@
 done
 
 lemma unique_NB:
-     "[| Crypt(pubK A) {|Nonce NA, Nonce NB|} \<in> parts(spies s);
-         Crypt(pubK A'){|Nonce NA', Nonce NB|} \<in> parts(spies s);
+     "[| Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts(spies s);
+         Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies s);
          Nonce NB \<notin> analz (spies s);
          s \<in> reachable Nprg |]
       ==> A=A' & NA=NA'"
@@ -257,7 +257,7 @@
 lemma Spy_not_see_NB:
      "[| A \<notin> bad;  B \<notin> bad |]
   ==> Nprg \<in> Always
-              {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s &
+              {s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s &
                   (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set s)
                   --> Nonce NB \<notin> analz (spies s)}"
 apply ns_induct
@@ -280,7 +280,7 @@
      "[| A \<notin> bad;  B \<notin> bad |]
   ==> Nprg \<in> Always
               {s. Crypt (pubK B) (Nonce NB) \<in> parts (spies s) &
-                  Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s
+                  Says B A  (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s
                   --> (\<exists>C. Says A C (Crypt (pubK C) (Nonce NB)) \<in> set s)}"
   (*insert an invariant for use in some of the subgoals*)
 apply (insert Spy_not_see_NB [of A B NA NB], simp, ns_induct)
@@ -294,7 +294,7 @@
 text{*Can we strengthen the secrecy theorem?  NO*}
 lemma "[| A \<notin> bad;  B \<notin> bad |]
   ==> Nprg \<in> Always
-              {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s
+              {s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s
                   --> Nonce NB \<notin> analz (spies s)}"
 apply ns_induct
 apply auto
@@ -317,13 +317,13 @@
 [| A \<notin> bad; B \<notin> bad |]
 ==> Nprg
    \<in> Always
-       {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s -->
+       {s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s -->
            Nonce NB \<notin> analz (knows Spy s)}
  1. !!s B' C.
        [| A \<notin> bad; B \<notin> bad; s \<in> reachable Nprg
-          Says A C (Crypt (pubK C) {|Nonce NA, Agent A|}) \<in> set s;
-          Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s;
-          C \<in> bad; Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s;
+          Says A C (Crypt (pubK C) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s;
+          Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s;
+          C \<in> bad; Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s;
           Nonce NB \<notin> analz (knows Spy s) |]
        ==> False
 *)