# HG changeset patch
# User wenzelm
# Date 1451495848 -3600
# Node ID cdea44c775fa7177b33d54224eb34cf32708f123
# Parent  8fb53badad9923c5da181040f06129b616e4bb59
more symbols;

diff -r 8fb53badad99 -r cdea44c775fa src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Wed Dec 30 18:17:28 2015 +0100
@@ -47,21 +47,17 @@
          | Crypt  key msg   --{*Encryption, public- or shared-key*}
 
 
-text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
+text{*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*}
 syntax
-  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
-
-syntax (xsymbols)
   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
-
 translations
-  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
-  "{|x, y|}"      == "CONST MPair x y"
+  "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+  "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
 
 
 definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
     --{*Message Y paired with a MAC computed with the help of X*}
-    "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
     --{*Keys useful to decrypt elements of a message set*}
@@ -75,8 +71,8 @@
   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"
+  | 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"
 
 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
@@ -134,7 +130,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]:
@@ -151,7 +147,7 @@
 subsection{*Inductive relation "parts"*}
 
 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)
@@ -325,8 +321,8 @@
   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"
+  | 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"
 
@@ -340,7 +336,7 @@
 
 text{*Making it safe speeds up proofs*}
 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)
@@ -424,8 +420,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)
@@ -541,7 +537,7 @@
 
 text{*If there are no pairs or encryptions then analz does nothing*}
 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
@@ -572,7 +568,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{*Monotonicity*}
@@ -584,7 +580,7 @@
 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
 inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
-inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
+inductive_cases MPair_synth [elim!]: "\<lbrace>X,Y\<rbrace> \<in> synth H"
 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
 
 
diff -r 8fb53badad99 -r cdea44c775fa src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Wed Dec 30 18:17:28 2015 +0100
@@ -27,22 +27,18 @@
          | Crypt  key msg
 
 syntax
-  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
-
-syntax (xsymbols)
   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
-
 translations
-  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
-  "{|x, y|}"      == "CONST MPair x y"
+  "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+  "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
 
 inductive_set
   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"
+  | 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"
 
 inductive_set
@@ -50,8 +46,8 @@
   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"
+  | 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"
 
@@ -61,7 +57,7 @@
   where
     Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
   | Agent  [intro]:   "Agent agt \<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"
 
 primrec initState
@@ -172,13 +168,13 @@
 
 lemma [code]:
   "analz H = (let
-     H' = H \<union> (\<Union>((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
+     H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
    in if H' = H then H else analz H')"
 sorry
 
 lemma [code]:
   "parts H = (let
-     H' = H \<union> (\<Union>((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
+     H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
    in if H' = H then H else parts H')"
 sorry
 
diff -r 8fb53badad99 -r cdea44c775fa src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy	Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy	Wed Dec 30 18:17:28 2015 +0100
@@ -61,9 +61,9 @@
   assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
   assumes "evs = 
   [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
-   Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
-   Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
-   Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
+   Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>),
+   Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>),
+   Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>)]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
   shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
 proof -
   from assms show "A \<noteq> Spy" by auto
@@ -79,14 +79,14 @@
   qed
   then have "[?e2, ?e1, ?e0] : ns_public"
   proof (rule NS2)
-    show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
+    show "Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e1, ?e0]" by simp
     show " Nonce 1 ~: used [?e1, ?e0]" by eval
   qed
   then show "evs : ns_public"
   unfolding assms
   proof (rule NS3)
-    show "  Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
-    show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|})
+    show "  Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e2, ?e1, ?e0]" by simp
+    show "Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>)
     : set [?e2, ?e1, ?e0]" by simp
   qed
   from assms show "Nonce NB : analz (knows Spy evs)"
diff -r 8fb53badad99 -r cdea44c775fa src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy	Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy	Wed Dec 30 18:17:28 2015 +0100
@@ -57,9 +57,9 @@
   assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
   assumes "evs = 
   [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
-   Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
-   Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
-   Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
+   Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>),
+   Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>),
+   Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>)]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
   shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
 proof -
   from assms show "A \<noteq> Spy" by auto
@@ -71,19 +71,19 @@
   qed
   then have "[?e1, ?e0] : ns_public"
   proof (rule Fake)
-    show "Crypt (pubEK Bob) {|Nonce 0, Agent Alice|} : synth (analz (knows Spy [?e0]))"
+    show "Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace> : synth (analz (knows Spy [?e0]))"
       by (intro synth.intros(2,3,4,1)) eval+
   qed
   then have "[?e2, ?e1, ?e0] : ns_public"
   proof (rule NS2)
-    show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
+    show "Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e1, ?e0]" by simp
     show " Nonce 1 ~: used [?e1, ?e0]" by eval
   qed
   then show "evs : ns_public"
   unfolding assms
   proof (rule NS3)
-    show "  Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
-    show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) : set [?e2, ?e1, ?e0]" by simp
+    show "  Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e2, ?e1, ?e0]" by simp
+    show "Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>) : set [?e2, ?e1, ?e0]" by simp
   qed
   from assms show "Nonce NB : analz (knows Spy evs)"
     apply simp
diff -r 8fb53badad99 -r cdea44c775fa src/HOL/SET_Protocol/Cardholder_Registration.thy
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Wed Dec 30 18:17:28 2015 +0100
@@ -38,7 +38,7 @@
         Says A B Z =>
          ((\<exists>N X Y. A \<noteq> Spy &
                  DK \<in> symKeys &
-                 Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) |
+                 Z = \<lbrace>Crypt DK \<lbrace>Agent A, Nonce N, Key K, X\<rbrace>, Y\<rbrace>) |
           (\<exists>C. DK = priEK C))
       | Gets A' X => False
       | Notes A' X => False))"
@@ -67,18 +67,18 @@
       Says A B Z =>
        A \<noteq> Spy &
        ((\<exists>X Y. DK \<in> symKeys &
-               Z = (EXHcrypt DK X {|Agent A, Nonce N|} Y)) |
+               Z = (EXHcrypt DK X \<lbrace>Agent A, Nonce N\<rbrace> Y)) |
         (\<exists>X Y. DK \<in> symKeys &
-               Z = {|Crypt DK {|Agent A, Nonce N, X|}, Y|}) |
+               Z = \<lbrace>Crypt DK \<lbrace>Agent A, Nonce N, X\<rbrace>, Y\<rbrace>) |
         (\<exists>K i X Y.
           K \<in> symKeys &
-          Z = Crypt K {|sign (priSK (CA i)) {|Agent B, Nonce N, X|}, Y|} &
+          Z = Crypt K \<lbrace>sign (priSK (CA i)) \<lbrace>Agent B, Nonce N, X\<rbrace>, Y\<rbrace> &
           (DK=K | KeyCryptKey DK K evs)) |
         (\<exists>K C NC3 Y.
           K \<in> symKeys &
           Z = Crypt K
-                {|sign (priSK C) {|Agent B, Nonce NC3, Agent C, Nonce N|},
-                  Y|} &
+                \<lbrace>sign (priSK C) \<lbrace>Agent B, Nonce NC3, Agent C, Nonce N\<rbrace>,
+                  Y\<rbrace> &
           (DK=K | KeyCryptKey DK K evs)) |
         (\<exists>C. DK = priEK C))
     | Gets A' X => False
@@ -104,15 +104,15 @@
 
 | SET_CR1: --{*CardCInitReq: C initiates a run, sending a nonce to CCA*}
              "[| evs1 \<in> set_cr;  C = Cardholder k;  Nonce NC1 \<notin> used evs1 |]
-              ==> Says C (CA i) {|Agent C, Nonce NC1|} # evs1 \<in> set_cr"
+              ==> Says C (CA i) \<lbrace>Agent C, Nonce NC1\<rbrace> # evs1 \<in> set_cr"
 
 | SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
              "[| evs2 \<in> set_cr;
-                 Gets (CA i) {|Agent C, Nonce NC1|} \<in> set evs2 |]
+                 Gets (CA i) \<lbrace>Agent C, Nonce NC1\<rbrace> \<in> set evs2 |]
               ==> Says (CA i) C
-                       {|sign (priSK (CA i)) {|Agent C, Nonce NC1|},
+                       \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC1\<rbrace>,
                          cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
-                         cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
+                         cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>
                     # evs2 \<in> set_cr"
 
 | SET_CR3:
@@ -125,18 +125,18 @@
     - certificates pertain to the CA that C contacted (this is done by
       checking the signature).
    C generates a fresh symmetric key KC1.
-   The point of encrypting @{term "{|Agent C, Nonce NC2, Hash (Pan(pan C))|}"}
+   The point of encrypting @{term "\<lbrace>Agent C, Nonce NC2, Hash (Pan(pan C))\<rbrace>"}
    is not clear. *}
 "[| evs3 \<in> set_cr;  C = Cardholder k;
     Nonce NC2 \<notin> used evs3;
     Key KC1 \<notin> used evs3; KC1 \<in> symKeys;
-    Gets C {|sign (invKey SKi) {|Agent X, Nonce NC1|},
+    Gets C \<lbrace>sign (invKey SKi) \<lbrace>Agent X, Nonce NC1\<rbrace>,
              cert (CA i) EKi onlyEnc (priSK RCA),
-             cert (CA i) SKi onlySig (priSK RCA)|}
+             cert (CA i) SKi onlySig (priSK RCA)\<rbrace>
        \<in> set evs3;
-    Says C (CA i) {|Agent C, Nonce NC1|} \<in> set evs3|]
- ==> Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
-       # Notes C {|Key KC1, Agent (CA i)|}
+    Says C (CA i) \<lbrace>Agent C, Nonce NC1\<rbrace> \<in> set evs3|]
+ ==> Says C (CA i) (EXHcrypt KC1 EKi \<lbrace>Agent C, Nonce NC2\<rbrace> (Pan(pan C)))
+       # Notes C \<lbrace>Key KC1, Agent (CA i)\<rbrace>
        # evs3 \<in> set_cr"
 
 | SET_CR4:
@@ -147,12 +147,12 @@
        envelope (here, KC1) *}
 "[| evs4 \<in> set_cr;
     Nonce NCA \<notin> used evs4;  KC1 \<in> symKeys;
-    Gets (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan X)))
+    Gets (CA i) (EXHcrypt KC1 EKi \<lbrace>Agent C, Nonce NC2\<rbrace> (Pan(pan X)))
        \<in> set evs4 |]
   ==> Says (CA i) C
-          {|sign (priSK (CA i)) {|Agent C, Nonce NC2, Nonce NCA|},
+          \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>,
             cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
-            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
+            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>
        # evs4 \<in> set_cr"
 
 | SET_CR5:
@@ -165,21 +165,21 @@
     Nonce NC3 \<notin> used evs5;  Nonce CardSecret \<notin> used evs5; NC3\<noteq>CardSecret;
     Key KC2 \<notin> used evs5; KC2 \<in> symKeys;
     Key KC3 \<notin> used evs5; KC3 \<in> symKeys; KC2\<noteq>KC3;
-    Gets C {|sign (invKey SKi) {|Agent C, Nonce NC2, Nonce NCA|},
+    Gets C \<lbrace>sign (invKey SKi) \<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>,
              cert (CA i) EKi onlyEnc (priSK RCA),
-             cert (CA i) SKi onlySig (priSK RCA) |}
+             cert (CA i) SKi onlySig (priSK RCA) \<rbrace>
         \<in> set evs5;
-    Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
+    Says C (CA i) (EXHcrypt KC1 EKi \<lbrace>Agent C, Nonce NC2\<rbrace> (Pan(pan C)))
          \<in> set evs5 |]
 ==> Says C (CA i)
-         {|Crypt KC3
-             {|Agent C, Nonce NC3, Key KC2, Key (pubSK C),
+         \<lbrace>Crypt KC3
+             \<lbrace>Agent C, Nonce NC3, Key KC2, Key (pubSK C),
                Crypt (priSK C)
-                 (Hash {|Agent C, Nonce NC3, Key KC2,
-                         Key (pubSK C), Pan (pan C), Nonce CardSecret|})|},
-           Crypt EKi {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
-    # Notes C {|Key KC2, Agent (CA i)|}
-    # Notes C {|Key KC3, Agent (CA i)|}
+                 (Hash \<lbrace>Agent C, Nonce NC3, Key KC2,
+                         Key (pubSK C), Pan (pan C), Nonce CardSecret\<rbrace>)\<rbrace>,
+           Crypt EKi \<lbrace>Key KC3, Pan (pan C), Nonce CardSecret\<rbrace> \<rbrace>
+    # Notes C \<lbrace>Key KC2, Agent (CA i)\<rbrace>
+    # Notes C \<lbrace>Key KC3, Agent (CA i)\<rbrace>
     # evs5 \<in> set_cr"
 
 
@@ -197,18 +197,18 @@
     KC2 \<in> symKeys;  KC3 \<in> symKeys;  cardSK \<notin> symKeys;
     Notes (CA i) (Key cardSK) \<notin> set evs6;
     Gets (CA i)
-      {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, Key cardSK,
+      \<lbrace>Crypt KC3 \<lbrace>Agent C, Nonce NC3, Key KC2, Key cardSK,
                     Crypt (invKey cardSK)
-                      (Hash {|Agent C, Nonce NC3, Key KC2,
-                              Key cardSK, Pan (pan C), Nonce CardSecret|})|},
-        Crypt (pubEK (CA i)) {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
+                      (Hash \<lbrace>Agent C, Nonce NC3, Key KC2,
+                              Key cardSK, Pan (pan C), Nonce CardSecret\<rbrace>)\<rbrace>,
+        Crypt (pubEK (CA i)) \<lbrace>Key KC3, Pan (pan C), Nonce CardSecret\<rbrace> \<rbrace>
       \<in> set evs6 |]
 ==> Says (CA i) C
          (Crypt KC2
-          {|sign (priSK (CA i))
-                 {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
+          \<lbrace>sign (priSK (CA i))
+                 \<lbrace>Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA\<rbrace>,
             certC (pan C) cardSK (XOR(CardSecret,NonceCCA)) onlySig (priSK (CA i)),
-            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
+            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>)
       # Notes (CA i) (Key cardSK)
       # evs6 \<in> set_cr"
 
@@ -238,11 +238,11 @@
    ==> \<exists>evs \<in> set_cr.
        Says (CA i) C
             (Crypt KC2
-             {|sign (priSK (CA i))
-                    {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
+             \<lbrace>sign (priSK (CA i))
+                    \<lbrace>Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA\<rbrace>,
                certC (pan C) (pubSK (Cardholder k)) (XOR(CardSecret,NonceCCA))
                      onlySig (priSK (CA i)),
-               cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
+               cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>)
           \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] 
@@ -297,7 +297,7 @@
 text{*Trivial in the current model, where certificates by RCA are secure *}
 
 lemma Crypt_valid_pubEK:
-     "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
+     "[| Crypt (priSK RCA) \<lbrace>Agent C, Key EKi, onlyEnc\<rbrace>
            \<in> parts (knows Spy evs);
          evs \<in> set_cr |] ==> EKi = pubEK C"
 apply (erule rev_mp)
@@ -313,7 +313,7 @@
 done
 
 lemma Crypt_valid_pubSK:
-     "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
+     "[| Crypt (priSK RCA) \<lbrace>Agent C, Key SKi, onlySig\<rbrace>
            \<in> parts (knows Spy evs);
          evs \<in> set_cr |] ==> SKi = pubSK C"
 apply (erule rev_mp)
@@ -328,8 +328,8 @@
 done
 
 lemma Gets_certificate_valid:
-     "[| Gets A {| X, cert C EKi onlyEnc (priSK RCA),
-                      cert C SKi onlySig (priSK RCA)|} \<in> set evs;
+     "[| Gets A \<lbrace> X, cert C EKi onlyEnc (priSK RCA),
+                      cert C SKi onlySig (priSK RCA)\<rbrace> \<in> set evs;
          evs \<in> set_cr |]
       ==> EKi = pubEK C & SKi = pubSK C"
 by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
@@ -387,10 +387,10 @@
 text{*Message @{text SET_CR2}: C can check CA's signature if he has received
      CA's certificate.*}
 lemma CA_Says_2_lemma:
-     "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC1|})
+     "[| Crypt (priSK (CA i)) (Hash\<lbrace>Agent C, Nonce NC1\<rbrace>)
            \<in> parts (knows Spy evs);
          evs \<in> set_cr; (CA i) \<notin> bad |]
-     ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
+     ==> \<exists>Y. Says (CA i) C \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC1\<rbrace>, Y\<rbrace>
                  \<in> set evs"
 apply (erule rev_mp)
 apply (erule set_cr.induct, auto)
@@ -398,11 +398,11 @@
 
 text{*Ever used?*}
 lemma CA_Says_2:
-     "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC1|})
+     "[| Crypt (invKey SK) (Hash\<lbrace>Agent C, Nonce NC1\<rbrace>)
            \<in> parts (knows Spy evs);
          cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
          evs \<in> set_cr; (CA i) \<notin> bad |]
-      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
+      ==> \<exists>Y. Says (CA i) C \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC1\<rbrace>, Y\<rbrace>
                   \<in> set evs"
 by (blast dest!: certificate_valid_pubSK intro!: CA_Says_2_lemma)
 
@@ -410,23 +410,23 @@
 text{*Message @{text SET_CR4}: C can check CA's signature if he has received
       CA's certificate.*}
 lemma CA_Says_4_lemma:
-     "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
+     "[| Crypt (priSK (CA i)) (Hash\<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>)
            \<in> parts (knows Spy evs);
          evs \<in> set_cr; (CA i) \<notin> bad |]
-      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
-                     {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
+      ==> \<exists>Y. Says (CA i) C \<lbrace>sign (priSK (CA i))
+                     \<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>, Y\<rbrace> \<in> set evs"
 apply (erule rev_mp)
 apply (erule set_cr.induct, auto)
 done
 
 text{*NEVER USED*}
 lemma CA_Says_4:
-     "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
+     "[| Crypt (invKey SK) (Hash\<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>)
            \<in> parts (knows Spy evs);
          cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
          evs \<in> set_cr; (CA i) \<notin> bad |]
-      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
-                   {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
+      ==> \<exists>Y. Says (CA i) C \<lbrace>sign (priSK (CA i))
+                   \<lbrace>Agent C, Nonce NC2, Nonce NCA\<rbrace>, Y\<rbrace> \<in> set evs"
 by (blast dest!: certificate_valid_pubSK intro!: CA_Says_4_lemma)
 
 
@@ -434,23 +434,23 @@
       received CA's certificate.*}
 lemma CA_Says_6_lemma:
      "[| Crypt (priSK (CA i)) 
-               (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
+               (Hash\<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA\<rbrace>)
            \<in> parts (knows Spy evs);
          evs \<in> set_cr; (CA i) \<notin> bad |]
-      ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
-      {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
+      ==> \<exists>Y K. Says (CA i) C (Crypt K \<lbrace>sign (priSK (CA i))
+      \<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA\<rbrace>, Y\<rbrace>) \<in> set evs"
 apply (erule rev_mp)
 apply (erule set_cr.induct, auto)
 done
 
 text{*NEVER USED*}
 lemma CA_Says_6:
-     "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
+     "[| Crypt (invKey SK) (Hash\<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA\<rbrace>)
            \<in> parts (knows Spy evs);
          cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
          evs \<in> set_cr; (CA i) \<notin> bad |]
-      ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
-                    {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
+      ==> \<exists>Y K. Says (CA i) C (Crypt K \<lbrace>sign (priSK (CA i))
+                    \<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA\<rbrace>, Y\<rbrace>) \<in> set evs"
 by (blast dest!: certificate_valid_pubSK intro!: CA_Says_6_lemma)
 (*>*)
 
@@ -521,7 +521,7 @@
   message 5 in the same way, but the current model assumes that rule
   @{text SET_CR5} is executed only by honest agents.*}
 lemma msg6_KeyCryptKey_disj:
-     "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
+     "[|Gets B \<lbrace>Crypt KC3 \<lbrace>Agent C, Nonce N, Key KC2, Key cardSK, X\<rbrace>, Y\<rbrace>
           \<in> set evs;
         cardSK \<notin> symKeys;  evs \<in> set_cr|]
       ==> Key cardSK \<in> analz (knows Spy evs) |
@@ -602,12 +602,12 @@
 
 text{*Lemma concerning the actual signed message digest*}
 lemma cert_valid_lemma:
-     "[|Crypt (priSK (CA i)) {|Hash {|Nonce N, Pan(pan C)|}, Key cardSK, N1|}
+     "[|Crypt (priSK (CA i)) \<lbrace>Hash \<lbrace>Nonce N, Pan(pan C)\<rbrace>, Key cardSK, N1\<rbrace>
           \<in> parts (knows Spy evs);
         CA i \<notin> bad; evs \<in> set_cr|]
   ==> \<exists>KC2 X Y. Says (CA i) C
                      (Crypt KC2 
-                       {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
+                       \<lbrace>X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y\<rbrace>)
                   \<in> set evs"
 apply (erule rev_mp)
 apply (erule set_cr.induct)
@@ -618,12 +618,12 @@
 text{*Pre-packaged version for cardholder.  We don't try to confirm the values
   of KC2, X and Y, since they are not important.*}
 lemma certificate_valid_cardSK:
-    "[|Gets C (Crypt KC2 {|X, certC (pan C) cardSK N onlySig (invKey SKi),
-                              cert (CA i) SKi onlySig (priSK RCA)|}) \<in> set evs;
+    "[|Gets C (Crypt KC2 \<lbrace>X, certC (pan C) cardSK N onlySig (invKey SKi),
+                              cert (CA i) SKi onlySig (priSK RCA)\<rbrace>) \<in> set evs;
         CA i \<notin> bad; evs \<in> set_cr|]
   ==> \<exists>KC2 X Y. Says (CA i) C
                      (Crypt KC2 
-                       {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
+                       \<lbrace>X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y\<rbrace>)
                    \<in> set evs"
 by (force dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Body]
                     certificate_valid_pubSK cert_valid_lemma)
@@ -631,7 +631,7 @@
 
 lemma Hash_imp_parts [rule_format]:
      "evs \<in> set_cr
-      ==> Hash{|X, Nonce N|} \<in> parts (knows Spy evs) -->
+      ==> Hash\<lbrace>X, Nonce N\<rbrace> \<in> parts (knows Spy evs) -->
           Nonce N \<in> parts (knows Spy evs)"
 apply (erule set_cr.induct, force)
 apply (simp_all (no_asm_simp))
@@ -640,7 +640,7 @@
 
 lemma Hash_imp_parts2 [rule_format]:
      "evs \<in> set_cr
-      ==> Hash{|X, Nonce M, Y, Nonce N|} \<in> parts (knows Spy evs) -->
+      ==> Hash\<lbrace>X, Nonce M, Y, Nonce N\<rbrace> \<in> parts (knows Spy evs) -->
           Nonce M \<in> parts (knows Spy evs) & Nonce N \<in> parts (knows Spy evs)"
 apply (erule set_cr.induct, force)
 apply (simp_all (no_asm_simp))
@@ -696,7 +696,7 @@
 text{*Lemma for message 6: either cardSK is compromised (when we don't care)
   or else cardSK hasn't been used to encrypt K.*}
 lemma msg6_KeyCryptNonce_disj:
-     "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
+     "[|Gets B \<lbrace>Crypt KC3 \<lbrace>Agent C, Nonce N, Key KC2, Key cardSK, X\<rbrace>, Y\<rbrace>
           \<in> set evs;
         cardSK \<notin> symKeys;  evs \<in> set_cr|]
       ==> Key cardSK \<in> analz (knows Spy evs) |
@@ -751,12 +751,12 @@
 subsection{*Secrecy of CardSecret: the Cardholder's secret*}
 
 lemma NC2_not_CardSecret:
-     "[|Crypt EKj {|Key K, Pan p, Hash {|Agent D, Nonce N|}|}
+     "[|Crypt EKj \<lbrace>Key K, Pan p, Hash \<lbrace>Agent D, Nonce N\<rbrace>\<rbrace>
           \<in> parts (knows Spy evs);
         Key K \<notin> analz (knows Spy evs);
         Nonce N \<notin> analz (knows Spy evs);
        evs \<in> set_cr|]
-      ==> Crypt EKi {|Key K', Pan p', Nonce N|} \<notin> parts (knows Spy evs)"
+      ==> Crypt EKi \<lbrace>Key K', Pan p', Nonce N\<rbrace> \<notin> parts (knows Spy evs)"
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule rev_mp)
@@ -765,11 +765,11 @@
 done
 
 lemma KC2_secure_lemma [rule_format]:
-     "[|U = Crypt KC3 {|Agent C, Nonce N, Key KC2, X|};
+     "[|U = Crypt KC3 \<lbrace>Agent C, Nonce N, Key KC2, X\<rbrace>;
         U \<in> parts (knows Spy evs);
         evs \<in> set_cr|]
   ==> Nonce N \<notin> analz (knows Spy evs) -->
-      (\<exists>k i W. Says (Cardholder k) (CA i) {|U,W|} \<in> set evs & 
+      (\<exists>k i W. Says (Cardholder k) (CA i) \<lbrace>U,W\<rbrace> \<in> set evs & 
                Cardholder k \<notin> bad & CA i \<notin> bad)"
 apply (erule_tac P = "U \<in> H" for H in rev_mp)
 apply (erule set_cr.induct)
@@ -783,7 +783,7 @@
 done
 
 lemma KC2_secrecy:
-     "[|Gets B {|Crypt K {|Agent C, Nonce N, Key KC2, X|}, Y|} \<in> set evs;
+     "[|Gets B \<lbrace>Crypt K \<lbrace>Agent C, Nonce N, Key KC2, X\<rbrace>, Y\<rbrace> \<in> set evs;
         Nonce N \<notin> analz (knows Spy evs);  KC2 \<in> symKeys;
         evs \<in> set_cr|]
        ==> Key KC2 \<notin> analz (knows Spy evs)"
@@ -794,7 +794,7 @@
 lemma CardSecret_secrecy_lemma [rule_format]:
      "[|CA i \<notin> bad;  evs \<in> set_cr|]
       ==> Key K \<notin> analz (knows Spy evs) -->
-          Crypt (pubEK (CA i)) {|Key K, Pan p, Nonce CardSecret|}
+          Crypt (pubEK (CA i)) \<lbrace>Key K, Pan p, Nonce CardSecret\<rbrace>
              \<in> parts (knows Spy evs) -->
           Nonce CardSecret \<notin> analz (knows Spy evs)"
 apply (erule set_cr.induct, analz_mono_contra)
@@ -825,9 +825,9 @@
 lemma CardSecret_secrecy:
      "[|Cardholder k \<notin> bad;  CA i \<notin> bad;
         Says (Cardholder k) (CA i)
-           {|X, Crypt EKi {|Key KC3, Pan p, Nonce CardSecret|}|} \<in> set evs;
-        Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
-                    cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
+           \<lbrace>X, Crypt EKi \<lbrace>Key KC3, Pan p, Nonce CardSecret\<rbrace>\<rbrace> \<in> set evs;
+        Gets A \<lbrace>Z, cert (CA i) EKi onlyEnc (priSK RCA),
+                    cert (CA i) SKi onlySig (priSK RCA)\<rbrace> \<in> set evs;
         KC3 \<in> symKeys;  evs \<in> set_cr|]
       ==> Nonce CardSecret \<notin> analz (knows Spy evs)"
 apply (frule Gets_certificate_valid, assumption)
@@ -841,11 +841,11 @@
 subsection{*Secrecy of NonceCCA [the CA's secret] *}
 
 lemma NC2_not_NonceCCA:
-     "[|Hash {|Agent C', Nonce N', Agent C, Nonce N|}
+     "[|Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace>
           \<in> parts (knows Spy evs);
         Nonce N \<notin> analz (knows Spy evs);
        evs \<in> set_cr|]
-      ==> Crypt KC1 {|{|Agent B, Nonce N|}, Hash p|} \<notin> parts (knows Spy evs)"
+      ==> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs)"
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule set_cr.induct, analz_mono_contra, simp_all)
@@ -858,9 +858,9 @@
      "[|CA i \<notin> bad;  evs \<in> set_cr|]
       ==> Key K \<notin> analz (knows Spy evs) -->
           Crypt K
-            {|sign (priSK (CA i))
-                   {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
-              X, Y|}
+            \<lbrace>sign (priSK (CA i))
+                   \<lbrace>Agent C, Nonce N, Agent(CA i), Nonce NonceCCA\<rbrace>,
+              X, Y\<rbrace>
              \<in> parts (knows Spy evs) -->
           Nonce NonceCCA \<notin> analz (knows Spy evs)"
 apply (erule set_cr.induct, analz_mono_contra)
@@ -891,12 +891,12 @@
      "[|Cardholder k \<notin> bad;  CA i \<notin> bad;
         Gets (Cardholder k)
            (Crypt KC2
-            {|sign (priSK (CA i)) {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
-              X, Y|}) \<in> set evs;
+            \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce N, Agent(CA i), Nonce NonceCCA\<rbrace>,
+              X, Y\<rbrace>) \<in> set evs;
         Says (Cardholder k) (CA i)
-           {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, X'|}, Y'|} \<in> set evs;
-        Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
-                    cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
+           \<lbrace>Crypt KC3 \<lbrace>Agent C, Nonce NC3, Key KC2, X'\<rbrace>, Y'\<rbrace> \<in> set evs;
+        Gets A \<lbrace>Z, cert (CA i) EKi onlyEnc (priSK RCA),
+                    cert (CA i) SKi onlySig (priSK RCA)\<rbrace> \<in> set evs;
         KC2 \<in> symKeys;  evs \<in> set_cr|]
       ==> Nonce NonceCCA \<notin> analz (knows Spy evs)"
 apply (frule Gets_certificate_valid, assumption)
@@ -917,7 +917,7 @@
   and so the Spy knows that key already.  Either way, we can simplify
   the expression @{term "analz (insert (Key cardSK) X)"}.*}
 lemma msg6_cardSK_disj:
-     "[|Gets A {|Crypt K {|c, n, k', Key cardSK, X|}, Y|}
+     "[|Gets A \<lbrace>Crypt K \<lbrace>c, n, k', Key cardSK, X\<rbrace>, Y\<rbrace>
           \<in> set evs;  evs \<in> set_cr |]
       ==> cardSK \<notin> range(invKey o pubEK o CA) | Key cardSK \<in> knows Spy evs"
 by auto
@@ -961,7 +961,7 @@
 lemma pan_confidentiality:
      "[| Pan (pan C) \<in> analz(knows Spy evs); C \<noteq>Spy; evs :set_cr|]
     ==> \<exists>i X K HN.
-        Says C (CA i) {|X, Crypt (pubEK (CA i)) {|Key K, Pan (pan C), HN|} |}
+        Says C (CA i) \<lbrace>X, Crypt (pubEK (CA i)) \<lbrace>Key K, Pan (pan C), HN\<rbrace> \<rbrace>
            \<in> set evs
       & (CA i) \<in> bad"
 apply (erule rev_mp)
@@ -985,9 +985,9 @@
 
 lemma CR6_Says_imp_Notes:
      "[|Says (CA i) C (Crypt KC2
-          {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
+          \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce Y\<rbrace>,
             certC (pan C) cardSK X onlySig (priSK (CA i)),
-            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})  \<in> set evs;
+            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>)  \<in> set evs;
         evs \<in> set_cr |]
       ==> Notes (CA i) (Key cardSK) \<in> set evs"
 apply (erule rev_mp)
@@ -999,14 +999,14 @@
       This holds because a CA accepts a cardSK at most once.*}
 lemma cardholder_key_unicity:
      "[|Says (CA i) C (Crypt KC2
-          {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
+          \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C, Nonce NC3, Agent (CA i), Nonce Y\<rbrace>,
             certC (pan C) cardSK X onlySig (priSK (CA i)),
-            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
+            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>)
           \<in> set evs;
         Says (CA i) C' (Crypt KC2'
-          {|sign (priSK (CA i)) {|Agent C', Nonce NC3', Agent (CA i), Nonce Y'|},
+          \<lbrace>sign (priSK (CA i)) \<lbrace>Agent C', Nonce NC3', Agent (CA i), Nonce Y'\<rbrace>,
             certC (pan C') cardSK X' onlySig (priSK (CA i)),
-            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
+            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>)
           \<in> set evs;
         evs \<in> set_cr |] ==> C=C' & NC3=NC3' & X=X' & KC2=KC2' & Y=Y'"
 apply (erule rev_mp)
@@ -1020,9 +1020,9 @@
 (*<*)
 text{*UNUSED unicity result*}
 lemma unique_KC1:
-     "[|Says C B {|Crypt KC1 X, Crypt EK {|Key KC1, Y|}|}
+     "[|Says C B \<lbrace>Crypt KC1 X, Crypt EK \<lbrace>Key KC1, Y\<rbrace>\<rbrace>
           \<in> set evs;
-        Says C B' {|Crypt KC1 X', Crypt EK' {|Key KC1, Y'|}|}
+        Says C B' \<lbrace>Crypt KC1 X', Crypt EK' \<lbrace>Key KC1, Y'\<rbrace>\<rbrace>
           \<in> set evs;
         C \<notin> bad;  evs \<in> set_cr|] ==> B'=B & Y'=Y"
 apply (erule rev_mp)
@@ -1032,8 +1032,8 @@
 
 text{*UNUSED unicity result*}
 lemma unique_KC2:
-     "[|Says C B {|Crypt K {|Agent C, nn, Key KC2, X|}, Y|} \<in> set evs;
-        Says C B' {|Crypt K' {|Agent C, nn', Key KC2, X'|}, Y'|} \<in> set evs;
+     "[|Says C B \<lbrace>Crypt K \<lbrace>Agent C, nn, Key KC2, X\<rbrace>, Y\<rbrace> \<in> set evs;
+        Says C B' \<lbrace>Crypt K' \<lbrace>Agent C, nn', Key KC2, X'\<rbrace>, Y'\<rbrace> \<in> set evs;
         C \<notin> bad;  evs \<in> set_cr|] ==> B'=B & X'=X"
 apply (erule rev_mp)
 apply (erule rev_mp)
diff -r 8fb53badad99 -r cdea44c775fa src/HOL/SET_Protocol/Merchant_Registration.thy
--- a/src/HOL/SET_Protocol/Merchant_Registration.thy	Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/SET_Protocol/Merchant_Registration.thy	Wed Dec 30 18:17:28 2015 +0100
@@ -36,16 +36,16 @@
 
 | SET_MR1: --{*RegFormReq: M requires a registration form to a CA*}
            "[| evs1 \<in> set_mr; M = Merchant k; Nonce NM1 \<notin> used evs1 |]
-            ==> Says M (CA i) {|Agent M, Nonce NM1|} # evs1 \<in> set_mr"
+            ==> Says M (CA i) \<lbrace>Agent M, Nonce NM1\<rbrace> # evs1 \<in> set_mr"
 
 
 | SET_MR2: --{*RegFormRes: CA replies with the registration form and the 
                certificates for her keys*}
   "[| evs2 \<in> set_mr; Nonce NCA \<notin> used evs2;
-      Gets (CA i) {|Agent M, Nonce NM1|} \<in> set evs2 |]
-   ==> Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM1, Nonce NCA|},
+      Gets (CA i) \<lbrace>Agent M, Nonce NM1\<rbrace> \<in> set evs2 |]
+   ==> Says (CA i) M \<lbrace>sign (priSK (CA i)) \<lbrace>Agent M, Nonce NM1, Nonce NCA\<rbrace>,
                        cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
-                       cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) |}
+                       cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) \<rbrace>
          # evs2 \<in> set_mr"
 
 | SET_MR3:
@@ -57,16 +57,16 @@
              in the model*}
   "[| evs3 \<in> set_mr; M = Merchant k; Nonce NM2 \<notin> used evs3;
       Key KM1 \<notin> used evs3;  KM1 \<in> symKeys;
-      Gets M {|sign (invKey SKi) {|Agent X, Nonce NM1, Nonce NCA|},
+      Gets M \<lbrace>sign (invKey SKi) \<lbrace>Agent X, Nonce NM1, Nonce NCA\<rbrace>,
                cert (CA i) EKi onlyEnc (priSK RCA),
-               cert (CA i) SKi onlySig (priSK RCA) |}
+               cert (CA i) SKi onlySig (priSK RCA) \<rbrace>
         \<in> set evs3;
-      Says M (CA i) {|Agent M, Nonce NM1|} \<in> set evs3 |]
+      Says M (CA i) \<lbrace>Agent M, Nonce NM1\<rbrace> \<in> set evs3 |]
    ==> Says M (CA i)
-            {|Crypt KM1 (sign (priSK M) {|Agent M, Nonce NM2,
-                                          Key (pubSK M), Key (pubEK M)|}),
-              Crypt EKi (Key KM1)|}
-         # Notes M {|Key KM1, Agent (CA i)|}
+            \<lbrace>Crypt KM1 (sign (priSK M) \<lbrace>Agent M, Nonce NM2,
+                                          Key (pubSK M), Key (pubEK M)\<rbrace>),
+              Crypt EKi (Key KM1)\<rbrace>
+         # Notes M \<lbrace>Key KM1, Agent (CA i)\<rbrace>
          # evs3 \<in> set_mr"
 
 | SET_MR4:
@@ -80,14 +80,14 @@
         merSK \<notin> symKeys;  merEK \<notin> symKeys;
         Notes (CA i) (Key merSK) \<notin> set evs4;
         Notes (CA i) (Key merEK) \<notin> set evs4;
-        Gets (CA i) {|Crypt KM1 (sign (invKey merSK)
-                                 {|Agent M, Nonce NM2, Key merSK, Key merEK|}),
-                      Crypt (pubEK (CA i)) (Key KM1) |}
+        Gets (CA i) \<lbrace>Crypt KM1 (sign (invKey merSK)
+                                 \<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>),
+                      Crypt (pubEK (CA i)) (Key KM1) \<rbrace>
           \<in> set evs4 |]
-    ==> Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent(CA i)|},
+    ==> Says (CA i) M \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M, Nonce NM2, Agent(CA i)\<rbrace>,
                         cert  M      merSK    onlySig (priSK (CA i)),
                         cert  M      merEK    onlyEnc (priSK (CA i)),
-                        cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
+                        cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace>
           # Notes (CA i) (Key merSK)
           # Notes (CA i) (Key merEK)
           # evs4 \<in> set_mr"
@@ -148,7 +148,7 @@
   they hold, as in CR, because RCA's keys are secure*}
 
 lemma Crypt_valid_pubEK:
-     "[| Crypt (priSK RCA) {|Agent (CA i), Key EKi, onlyEnc|}
+     "[| Crypt (priSK RCA) \<lbrace>Agent (CA i), Key EKi, onlyEnc\<rbrace>
            \<in> parts (knows Spy evs);
          evs \<in> set_mr |] ==> EKi = pubEK (CA i)"
 apply (erule rev_mp)
@@ -164,7 +164,7 @@
 done
 
 lemma Crypt_valid_pubSK:
-     "[| Crypt (priSK RCA) {|Agent (CA i), Key SKi, onlySig|}
+     "[| Crypt (priSK RCA) \<lbrace>Agent (CA i), Key SKi, onlySig\<rbrace>
            \<in> parts (knows Spy evs);
          evs \<in> set_mr |] ==> SKi = pubSK (CA i)"
 apply (erule rev_mp)
@@ -179,8 +179,8 @@
 done
 
 lemma Gets_certificate_valid:
-     "[| Gets A {| X, cert (CA i) EKi onlyEnc (priSK RCA),
-                      cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
+     "[| Gets A \<lbrace> X, cert (CA i) EKi onlyEnc (priSK RCA),
+                      cert (CA i) SKi onlySig (priSK RCA)\<rbrace> \<in> set evs;
          evs \<in> set_mr |]
       ==> EKi = pubEK (CA i) & SKi = pubSK (CA i)"
 by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
@@ -261,9 +261,9 @@
 text{*Lemma for message 4: either merK is compromised (when we don't care)
   or else merK hasn't been used to encrypt K.*}
 lemma msg4_priEK_disj:
-     "[|Gets B {|Crypt KM1
-                       (sign K {|Agent M, Nonce NM2, Key merSK, Key merEK|}),
-                 Y|} \<in> set evs;
+     "[|Gets B \<lbrace>Crypt KM1
+                       (sign K \<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>),
+                 Y\<rbrace> \<in> set evs;
         evs \<in> set_mr|]
   ==> (Key merSK \<in> analz (knows Spy evs) | merSK \<notin> range(\<lambda>C. priEK C))
    &  (Key merEK \<in> analz (knows Spy evs) | merEK \<notin> range(\<lambda>C. priEK C))"
@@ -320,10 +320,10 @@
 subsection{*Unicity *}
 
 lemma msg4_Says_imp_Notes:
- "[|Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
+ "[|Says (CA i) M \<lbrace>sign (priSK (CA i)) \<lbrace>Agent M, Nonce NM2, Agent (CA i)\<rbrace>,
                     cert  M      merSK    onlySig (priSK (CA i)),
                     cert  M      merEK    onlyEnc (priSK (CA i)),
-                    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
+                    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
     evs \<in> set_mr |]
   ==> Notes (CA i) (Key merSK) \<in> set evs
    &  Notes (CA i) (Key merEK) \<in> set evs"
@@ -335,14 +335,14 @@
 text{*Unicity of merSK wrt a given CA:
   merSK uniquely identifies the other components, including merEK*}
 lemma merSK_unicity:
- "[|Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
+ "[|Says (CA i) M \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M, Nonce NM2, Agent (CA i)\<rbrace>,
                     cert  M      merSK    onlySig (priSK (CA i)),
                     cert  M      merEK    onlyEnc (priSK (CA i)),
-                    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
-    Says (CA i) M' {|sign (priSK(CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
+                    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
+    Says (CA i) M' \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M', Nonce NM2', Agent (CA i)\<rbrace>,
                     cert  M'      merSK    onlySig (priSK (CA i)),
                     cert  M'      merEK'    onlyEnc (priSK (CA i)),
-                    cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)|} \<in> set evs;
+                    cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
     evs \<in> set_mr |] ==> M=M' & NM2=NM2' & merEK=merEK'"
 apply (erule rev_mp)
 apply (erule rev_mp)
@@ -354,14 +354,14 @@
 text{*Unicity of merEK wrt a given CA:
   merEK uniquely identifies the other components, including merSK*}
 lemma merEK_unicity:
- "[|Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
+ "[|Says (CA i) M \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M, Nonce NM2, Agent (CA i)\<rbrace>,
                     cert  M      merSK    onlySig (priSK (CA i)),
                     cert  M      merEK    onlyEnc (priSK (CA i)),
-                    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
-    Says (CA i) M' {|sign (priSK(CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
+                    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
+    Says (CA i) M' \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M', Nonce NM2', Agent (CA i)\<rbrace>,
                      cert  M'      merSK'    onlySig (priSK (CA i)),
                      cert  M'      merEK    onlyEnc (priSK (CA i)),
-                     cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)|} \<in> set evs;
+                     cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
     evs \<in> set_mr |] 
   ==> M=M' & NM2=NM2' & merSK=merSK'"
 apply (erule rev_mp)
@@ -386,11 +386,11 @@
 text{*The assumption @{term "CA i \<noteq> RCA"} is required: step 2 uses 
   certificates of the same form.*}
 lemma certificate_merSK_valid_lemma [intro]:
-     "[|Crypt (priSK (CA i)) {|Agent M, Key merSK, onlySig|}
+     "[|Crypt (priSK (CA i)) \<lbrace>Agent M, Key merSK, onlySig\<rbrace>
           \<in> parts (knows Spy evs);
         CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
  ==> \<exists>X Y Z. Says (CA i) M
-                  {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} \<in> set evs"
+                  \<lbrace>X, cert M merSK onlySig (priSK (CA i)), Y, Z\<rbrace> \<in> set evs"
 apply (erule rev_mp)
 apply (erule set_mr.induct)
 apply (simp_all (no_asm_simp))
@@ -401,15 +401,15 @@
      "[| cert M merSK onlySig (priSK (CA i)) \<in> parts (knows Spy evs);
          CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
  ==> \<exists>X Y Z. Says (CA i) M
-                  {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} \<in> set evs"
+                  \<lbrace>X, cert M merSK onlySig (priSK (CA i)), Y, Z\<rbrace> \<in> set evs"
 by auto
 
 lemma certificate_merEK_valid_lemma [intro]:
-     "[|Crypt (priSK (CA i)) {|Agent M, Key merEK, onlyEnc|}
+     "[|Crypt (priSK (CA i)) \<lbrace>Agent M, Key merEK, onlyEnc\<rbrace>
           \<in> parts (knows Spy evs);
         CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
  ==> \<exists>X Y Z. Says (CA i) M
-                  {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} \<in> set evs"
+                  \<lbrace>X, Y, cert M merEK onlyEnc (priSK (CA i)), Z\<rbrace> \<in> set evs"
 apply (erule rev_mp)
 apply (erule set_mr.induct)
 apply (simp_all (no_asm_simp))
@@ -420,7 +420,7 @@
      "[| cert M merEK onlyEnc (priSK (CA i)) \<in> parts (knows Spy evs);
          CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
  ==> \<exists>X Y Z. Says (CA i) M
-                  {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} \<in> set evs"
+                  \<lbrace>X, Y, cert M merEK onlyEnc (priSK (CA i)), Z\<rbrace> \<in> set evs"
 by auto
 
 text{*The two certificates - for merSK and for merEK - cannot be proved to
diff -r 8fb53badad99 -r cdea44c775fa src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Wed Dec 30 18:17:28 2015 +0100
@@ -67,16 +67,12 @@
          | Crypt  key msg   --{*Encryption, public- or shared-key*}
 
 
-(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
+(*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*)
 syntax
-  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
-
-syntax (xsymbols)
   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
-
 translations
-  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
-  "{|x, y|}"      == "CONST MPair x y"
+  "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+  "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
 
 
 definition nat_of_agent :: "agent => nat" where
@@ -104,8 +100,8 @@
   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"
+  | 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"
 
 
@@ -180,7 +176,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]:
@@ -197,7 +193,7 @@
 subsection{*Inductive relation "parts"*}
 
 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)
 
@@ -346,8 +342,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)
@@ -398,8 +394,8 @@
   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"
+  | 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"
 
@@ -413,7 +409,7 @@
 
 text{*Making it safe speeds up proofs*}
 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)
@@ -497,8 +493,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)
@@ -619,7 +615,7 @@
 
 (*If there are no pairs or encryptions then analz does nothing*)
 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
@@ -650,7 +646,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"
 
 (*Monotonicity*)
@@ -664,7 +660,7 @@
 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
 inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
-inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
+inductive_cases MPair_synth [elim!]: "\<lbrace>X,Y\<rbrace> \<in> synth H"
 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
 inductive_cases Pan_synth   [elim!]: "Pan A \<in> synth H"
 
@@ -790,7 +786,7 @@
 (*Without this equation, other rules for synth and analz would yield
   redundant cases*)
 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
 
@@ -802,7 +798,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
 
 
diff -r 8fb53badad99 -r cdea44c775fa src/HOL/SET_Protocol/Public_SET.thy
--- a/src/HOL/SET_Protocol/Public_SET.thy	Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/SET_Protocol/Public_SET.thy	Wed Dec 30 18:17:28 2015 +0100
@@ -128,7 +128,7 @@
 definition
  (* Signature = Message + signed Digest *)
   sign :: "[key, msg]=>msg"
-  where "sign K X = {|X, Crypt K (Hash X) |}"
+  where "sign K X = \<lbrace>X, Crypt K (Hash X) \<rbrace>"
 
 definition
  (* Signature Only = signed Digest Only *)
@@ -138,7 +138,7 @@
 definition
  (* Signature for Certificates = Message + signed Message *)
   signCert :: "[key, msg]=>msg"
-  where "signCert K X = {|X, Crypt K X |}"
+  where "signCert K X = \<lbrace>X, Crypt K X \<rbrace>"
 
 definition
  (* Certification Authority's Certificate.
@@ -149,7 +149,7 @@
                   then Ka=pubEK i or pubSK i depending on T  ??
  *)
   cert :: "[agent, key, msg, key] => msg"
-  where "cert A Ka T signK = signCert signK {|Agent A, Key Ka, T|}"
+  where "cert A Ka T signK = signCert signK \<lbrace>Agent A, Key Ka, T\<rbrace>"
 
 definition
  (* Cardholder's Certificate.
@@ -158,7 +158,7 @@
  *)
   certC :: "[nat, key, nat, msg, key] => msg"
   where "certC PAN Ka PS T signK =
-    signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}"
+    signCert signK \<lbrace>Hash \<lbrace>Nonce PS, Pan PAN\<rbrace>, Key Ka, T\<rbrace>"
 
 (*cert and certA have no repeated elements, so they could be abbreviations,
   but that's tricky and makes proofs slower*)
@@ -173,13 +173,13 @@
   --{*Extra Encryption*}
     (*K: the symmetric key   EK: the public encryption key*)
     "EXcrypt K EK M m =
-       {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m|}|}"
+       \<lbrace>Crypt K \<lbrace>M, Hash m\<rbrace>, Crypt EK \<lbrace>Key K, m\<rbrace>\<rbrace>"
 
 definition EXHcrypt :: "[key,key,msg,msg] => msg" where
   --{*Extra Encryption with Hashing*}
     (*K: the symmetric key   EK: the public encryption key*)
     "EXHcrypt K EK M m =
-       {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m, Hash M|}|}"
+       \<lbrace>Crypt K \<lbrace>M, Hash m\<rbrace>, Crypt EK \<lbrace>Key K, m, Hash M\<rbrace>\<rbrace>"
 
 definition Enc :: "[key,key,key,msg] => msg" where
   --{*Simple Encapsulation with SIGNATURE*}
@@ -187,12 +187,12 @@
       K: the symmetric key
       EK: the public encryption key*)
     "Enc SK K EK M =
-       {|Crypt K (sign SK M), Crypt EK (Key K)|}"
+       \<lbrace>Crypt K (sign SK M), Crypt EK (Key K)\<rbrace>"
 
 definition EncB :: "[key,key,key,msg,msg] => msg" where
   --{*Encapsulation with Baggage.  Keys as above, and baggage b.*}
     "EncB SK K EK M b =
-       {|Enc SK K EK {|M, Hash b|}, b|}"
+       \<lbrace>Enc SK K EK \<lbrace>M, Hash b\<rbrace>, b\<rbrace>"
 
 
 subsection{*Basic Properties of pubEK, pubSK, priEK and priSK *}
@@ -416,13 +416,13 @@
 text{*Avoids duplicating X and its components!*}
 lemma parts_insert_signCert:
      "parts (insert (signCert K X) H) =  
-      insert {|X, Crypt K X|} (parts (insert (Crypt K X) H))"
+      insert \<lbrace>X, Crypt K X\<rbrace> (parts (insert (Crypt K X) H))"
 by (simp add: signCert_def insert_commute [of X])
 
 text{*Avoids a case split! [X is always available]*}
 lemma analz_insert_signCert:
      "analz (insert (signCert K X) H) =  
-      insert {|X, Crypt K X|} (insert (Crypt K X) (analz (insert X H)))"
+      insert \<lbrace>X, Crypt K X\<rbrace> (insert (Crypt K X) (analz (insert X H)))"
 by (simp add: signCert_def insert_commute [of X])
 
 lemma keysFor_insert_signCert: "keysFor (insert (signCert K X) H) = keysFor H"
@@ -463,7 +463,7 @@
 
 lemma EncB_partsE: 
      "!!R. [|EncB SK K EK M b \<in> parts H;  
-             [|Crypt K (sign SK {|M, Hash b|}) \<in> parts H;  
+             [|Crypt K (sign SK \<lbrace>M, Hash b\<rbrace>) \<in> parts H;  
                Crypt EK (Key K) \<in> parts H;  
                b \<in> parts H|] ==> R|]  
            ==> R"
@@ -471,8 +471,8 @@
 
 lemma EXcrypt_partsE: 
      "!!R. [|EXcrypt K EK M m \<in> parts H;  
-             [|Crypt K {|M, Hash m|} \<in> parts H;  
-               Crypt EK {|Key K, m|} \<in> parts H|] ==> R|]  
+             [|Crypt K \<lbrace>M, Hash m\<rbrace> \<in> parts H;  
+               Crypt EK \<lbrace>Key K, m\<rbrace> \<in> parts H|] ==> R|]  
            ==> R"
 by (unfold EXcrypt_def, blast)
 
diff -r 8fb53badad99 -r cdea44c775fa src/HOL/SET_Protocol/Purchase.thy
--- a/src/HOL/SET_Protocol/Purchase.thy	Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/SET_Protocol/Purchase.thy	Wed Dec 30 18:17:28 2015 +0100
@@ -86,38 +86,38 @@
    "[|evsStart \<in> set_pur;
       Number LID_M \<notin> used evsStart;
       C = Cardholder k; M = Merchant i; P = PG j;
-      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
+      Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
       LID_M \<notin> range CardSecret;
       LID_M \<notin> range PANSecret |]
-     ==> Notes C {|Number LID_M, Transaction|}
-       # Notes M {|Number LID_M, Agent P, Transaction|}
+     ==> Notes C \<lbrace>Number LID_M, Transaction\<rbrace>
+       # Notes M \<lbrace>Number LID_M, Agent P, Transaction\<rbrace>
        # evsStart \<in> set_pur"
 
 | PInitReq:
      --{*Purchase initialization, page 72 of Formal Protocol Desc.*}
    "[|evsPIReq \<in> set_pur;
-      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
+      Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
       Nonce Chall_C \<notin> used evsPIReq;
       Chall_C \<notin> range CardSecret; Chall_C \<notin> range PANSecret;
-      Notes C {|Number LID_M, Transaction |} \<in> set evsPIReq |]
-    ==> Says C M {|Number LID_M, Nonce Chall_C|} # evsPIReq \<in> set_pur"
+      Notes C \<lbrace>Number LID_M, Transaction \<rbrace> \<in> set evsPIReq |]
+    ==> Says C M \<lbrace>Number LID_M, Nonce Chall_C\<rbrace> # evsPIReq \<in> set_pur"
 
 | PInitRes:
      --{*Merchant replies with his own label XID and the encryption
          key certificate of his chosen Payment Gateway. Page 74 of Formal
          Protocol Desc. We use @{text LID_M} to identify Cardholder*}
    "[|evsPIRes \<in> set_pur;
-      Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPIRes;
-      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
-      Notes M {|Number LID_M, Agent P, Transaction|} \<in> set evsPIRes;
+      Gets M \<lbrace>Number LID_M, Nonce Chall_C\<rbrace> \<in> set evsPIRes;
+      Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
+      Notes M \<lbrace>Number LID_M, Agent P, Transaction\<rbrace> \<in> set evsPIRes;
       Nonce Chall_M \<notin> used evsPIRes;
       Chall_M \<notin> range CardSecret; Chall_M \<notin> range PANSecret;
       Number XID \<notin> used evsPIRes;
       XID \<notin> range CardSecret; XID \<notin> range PANSecret|]
     ==> Says M C (sign (priSK M)
-                       {|Number LID_M, Number XID,
+                       \<lbrace>Number LID_M, Number XID,
                          Nonce Chall_C, Nonce Chall_M,
-                         cert P (pubEK P) onlyEnc (priSK RCA)|})
+                         cert P (pubEK P) onlyEnc (priSK RCA)\<rbrace>)
           # evsPIRes \<in> set_pur"
 
 | PReqUns:
@@ -125,34 +125,34 @@
         Page 79 of Formal Protocol Desc.
         Merchant never sees the amount in clear. This holds of the real
         protocol, where XID identifies the transaction. We omit
-        Hash{|Number XID, Nonce (CardSecret k)|} from PIHead because
+        \<open>Hash\<lbrace>Number XID, Nonce (CardSecret k)\<rbrace>\<close> from PIHead because
         the CardSecret is 0 and because AuthReq treated the unsigned case
         very differently from the signed one anyway.*}
    "!!Chall_C Chall_M OrderDesc P PurchAmt XID evsPReqU.
     [|evsPReqU \<in> set_pur;
       C = Cardholder k; CardSecret k = 0;
       Key KC1 \<notin> used evsPReqU;  KC1 \<in> symKeys;
-      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
-      HOD = Hash{|Number OrderDesc, Number PurchAmt|};
-      OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,Nonce Chall_M|};
-      PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|};
+      Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
+      HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace>;
+      OIData = \<lbrace>Number LID_M, Number XID, Nonce Chall_C, HOD,Nonce Chall_M\<rbrace>;
+      PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M\<rbrace>;
       Gets C (sign (priSK M)
-                   {|Number LID_M, Number XID,
+                   \<lbrace>Number LID_M, Number XID,
                      Nonce Chall_C, Nonce Chall_M,
-                     cert P EKj onlyEnc (priSK RCA)|})
+                     cert P EKj onlyEnc (priSK RCA)\<rbrace>)
         \<in> set evsPReqU;
-      Says C M {|Number LID_M, Nonce Chall_C|} \<in> set evsPReqU;
-      Notes C {|Number LID_M, Transaction|} \<in> set evsPReqU |]
+      Says C M \<lbrace>Number LID_M, Nonce Chall_C\<rbrace> \<in> set evsPReqU;
+      Notes C \<lbrace>Number LID_M, Transaction\<rbrace> \<in> set evsPReqU |]
     ==> Says C M
-             {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)),
-               OIData, Hash{|PIHead, Pan (pan C)|} |}
-          # Notes C {|Key KC1, Agent M|}
+             \<lbrace>EXHcrypt KC1 EKj \<lbrace>PIHead, Hash OIData\<rbrace> (Pan (pan C)),
+               OIData, Hash\<lbrace>PIHead, Pan (pan C)\<rbrace> \<rbrace>
+          # Notes C \<lbrace>Key KC1, Agent M\<rbrace>
           # evsPReqU \<in> set_pur"
 
 | PReqS:
       --{*SIGNED Purchase request.  Page 77 of Formal Protocol Desc.
           We could specify the equation
-          @{term "PIReqSigned = {| PIDualSigned, OIDualSigned |}"}, since the
+          @{term "PIReqSigned = \<lbrace> PIDualSigned, OIDualSigned \<rbrace>"}, since the
           Formal Desc. gives PIHead the same format in the unsigned case.
           However, there's little point, as P treats the signed and 
           unsigned cases differently.*}
@@ -162,25 +162,25 @@
     [|evsPReqS \<in> set_pur;
       C = Cardholder k;
       CardSecret k \<noteq> 0;  Key KC2 \<notin> used evsPReqS;  KC2 \<in> symKeys;
-      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
-      HOD = Hash{|Number OrderDesc, Number PurchAmt|};
-      OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, Nonce Chall_M|};
-      PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
-                  Hash{|Number XID, Nonce (CardSecret k)|}|};
-      PANData = {|Pan (pan C), Nonce (PANSecret k)|};
-      PIData = {|PIHead, PANData|};
-      PIDualSigned = {|sign (priSK C) {|Hash PIData, Hash OIData|},
-                       EXcrypt KC2 EKj {|PIHead, Hash OIData|} PANData|};
-      OIDualSigned = {|OIData, Hash PIData|};
+      Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
+      HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace>;
+      OIData = \<lbrace>Number LID_M, Number XID, Nonce Chall_C, HOD, Nonce Chall_M\<rbrace>;
+      PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+                  Hash\<lbrace>Number XID, Nonce (CardSecret k)\<rbrace>\<rbrace>;
+      PANData = \<lbrace>Pan (pan C), Nonce (PANSecret k)\<rbrace>;
+      PIData = \<lbrace>PIHead, PANData\<rbrace>;
+      PIDualSigned = \<lbrace>sign (priSK C) \<lbrace>Hash PIData, Hash OIData\<rbrace>,
+                       EXcrypt KC2 EKj \<lbrace>PIHead, Hash OIData\<rbrace> PANData\<rbrace>;
+      OIDualSigned = \<lbrace>OIData, Hash PIData\<rbrace>;
       Gets C (sign (priSK M)
-                   {|Number LID_M, Number XID,
+                   \<lbrace>Number LID_M, Number XID,
                      Nonce Chall_C, Nonce Chall_M,
-                     cert P EKj onlyEnc (priSK RCA)|})
+                     cert P EKj onlyEnc (priSK RCA)\<rbrace>)
         \<in> set evsPReqS;
-      Says C M {|Number LID_M, Nonce Chall_C|} \<in> set evsPReqS;
-      Notes C {|Number LID_M, Transaction|} \<in> set evsPReqS |]
-    ==> Says C M {|PIDualSigned, OIDualSigned|}
-          # Notes C {|Key KC2, Agent M|}
+      Says C M \<lbrace>Number LID_M, Nonce Chall_C\<rbrace> \<in> set evsPReqS;
+      Notes C \<lbrace>Number LID_M, Transaction\<rbrace> \<in> set evsPReqS |]
+    ==> Says C M \<lbrace>PIDualSigned, OIDualSigned\<rbrace>
+          # Notes C \<lbrace>Key KC2, Agent M\<rbrace>
           # evsPReqS \<in> set_pur"
 
   --{*Authorization Request.  Page 92 of Formal Protocol Desc.
@@ -188,22 +188,22 @@
 | AuthReq:
    "[| evsAReq \<in> set_pur;
        Key KM \<notin> used evsAReq;  KM \<in> symKeys;
-       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
-       HOD = Hash{|Number OrderDesc, Number PurchAmt|};
-       OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,
-                  Nonce Chall_M|};
+       Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
+       HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace>;
+       OIData = \<lbrace>Number LID_M, Number XID, Nonce Chall_C, HOD,
+                  Nonce Chall_M\<rbrace>;
        CardSecret k \<noteq> 0 -->
-         P_I = {|sign (priSK C) {|HPIData, Hash OIData|}, encPANData|};
-       Gets M {|P_I, OIData, HPIData|} \<in> set evsAReq;
-       Says M C (sign (priSK M) {|Number LID_M, Number XID,
+         P_I = \<lbrace>sign (priSK C) \<lbrace>HPIData, Hash OIData\<rbrace>, encPANData\<rbrace>;
+       Gets M \<lbrace>P_I, OIData, HPIData\<rbrace> \<in> set evsAReq;
+       Says M C (sign (priSK M) \<lbrace>Number LID_M, Number XID,
                                   Nonce Chall_C, Nonce Chall_M,
-                                  cert P EKj onlyEnc (priSK RCA)|})
+                                  cert P EKj onlyEnc (priSK RCA)\<rbrace>)
          \<in> set evsAReq;
-        Notes M {|Number LID_M, Agent P, Transaction|}
+        Notes M \<lbrace>Number LID_M, Agent P, Transaction\<rbrace>
            \<in> set evsAReq |]
     ==> Says M P
              (EncB (priSK M) KM (pubEK P)
-               {|Number LID_M, Number XID, Hash OIData, HOD|}   P_I)
+               \<lbrace>Number LID_M, Number XID, Hash OIData, HOD\<rbrace>   P_I)
           # evsAReq \<in> set_pur"
 
   --{*Authorization Response has two forms: for UNSIGNED and SIGNED PIs.
@@ -220,14 +220,14 @@
        C = Cardholder k; M = Merchant i;
        Key KP \<notin> used evsAResU;  KP \<in> symKeys;
        CardSecret k = 0;  KC1 \<in> symKeys;  KM \<in> symKeys;
-       PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|};
-       P_I = EXHcrypt KC1 EKj {|PIHead, HOIData|} (Pan (pan C));
+       PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M\<rbrace>;
+       P_I = EXHcrypt KC1 EKj \<lbrace>PIHead, HOIData\<rbrace> (Pan (pan C));
        Gets P (EncB (priSK M) KM (pubEK P)
-               {|Number LID_M, Number XID, HOIData, HOD|} P_I)
+               \<lbrace>Number LID_M, Number XID, HOIData, HOD\<rbrace> P_I)
            \<in> set evsAResU |]
    ==> Says P M
             (EncB (priSK P) KP (pubEK M)
-              {|Number LID_M, Number XID, Number PurchAmt|}
+              \<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>
               authCode)
        # evsAResU \<in> set_pur"
 
@@ -237,41 +237,41 @@
        C = Cardholder k;
        Key KP \<notin> used evsAResS;  KP \<in> symKeys;
        CardSecret k \<noteq> 0;  KC2 \<in> symKeys;  KM \<in> symKeys;
-       P_I = {|sign (priSK C) {|Hash PIData, HOIData|},
-               EXcrypt KC2 (pubEK P) {|PIHead, HOIData|} PANData|};
-       PANData = {|Pan (pan C), Nonce (PANSecret k)|};
-       PIData = {|PIHead, PANData|};
-       PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
-                  Hash{|Number XID, Nonce (CardSecret k)|}|};
+       P_I = \<lbrace>sign (priSK C) \<lbrace>Hash PIData, HOIData\<rbrace>,
+               EXcrypt KC2 (pubEK P) \<lbrace>PIHead, HOIData\<rbrace> PANData\<rbrace>;
+       PANData = \<lbrace>Pan (pan C), Nonce (PANSecret k)\<rbrace>;
+       PIData = \<lbrace>PIHead, PANData\<rbrace>;
+       PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+                  Hash\<lbrace>Number XID, Nonce (CardSecret k)\<rbrace>\<rbrace>;
        Gets P (EncB (priSK M) KM (pubEK P)
-                {|Number LID_M, Number XID, HOIData, HOD|}
+                \<lbrace>Number LID_M, Number XID, HOIData, HOD\<rbrace>
                P_I)
            \<in> set evsAResS |]
    ==> Says P M
             (EncB (priSK P) KP (pubEK M)
-              {|Number LID_M, Number XID, Number PurchAmt|}
+              \<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>
               authCode)
        # evsAResS \<in> set_pur"
 
 | PRes:
     --{*Purchase response.*}
    "[| evsPRes \<in> set_pur;  KP \<in> symKeys;  M = Merchant i;
-       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
+       Transaction = \<lbrace>Agent M, Agent C, Number OrderDesc, Number PurchAmt\<rbrace>;
        Gets M (EncB (priSK P) KP (pubEK M)
-              {|Number LID_M, Number XID, Number PurchAmt|}
+              \<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>
               authCode)
           \<in> set evsPRes;
-       Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPRes;
+       Gets M \<lbrace>Number LID_M, Nonce Chall_C\<rbrace> \<in> set evsPRes;
        Says M P
             (EncB (priSK M) KM (pubEK P)
-              {|Number LID_M, Number XID, Hash OIData, HOD|} P_I)
+              \<lbrace>Number LID_M, Number XID, Hash OIData, HOD\<rbrace> P_I)
          \<in> set evsPRes;
-       Notes M {|Number LID_M, Agent P, Transaction|}
+       Notes M \<lbrace>Number LID_M, Agent P, Transaction\<rbrace>
           \<in> set evsPRes
       |]
    ==> Says M C
-         (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C,
-                           Hash (Number PurchAmt)|})
+         (sign (priSK M) \<lbrace>Number LID_M, Number XID, Nonce Chall_C,
+                           Hash (Number PurchAmt)\<rbrace>)
          # evsPRes \<in> set_pur"
 
 
@@ -320,8 +320,8 @@
    ==> \<exists>evs \<in> set_pur.
           Says M C
                (sign (priSK M)
-                    {|Number LID_M, Number XID, Nonce Chall_C, 
-                      Hash (Number PurchAmt)|})
+                    \<lbrace>Number LID_M, Number XID, Nonce Chall_C, 
+                      Hash (Number PurchAmt)\<rbrace>)
                   \<in> set evs" 
 apply (intro exI bexI)
 apply (rule_tac [2]
@@ -356,8 +356,8 @@
         LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] 
    ==>  \<exists>evs \<in> set_pur.
             Says M C
-                 (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, 
-                                   Hash (Number PurchAmt)|})
+                 (sign (priSK M) \<lbrace>Number LID_M, Number XID, Nonce Chall_C, 
+                                   Hash (Number PurchAmt)\<rbrace>)
                \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2]
@@ -395,12 +395,12 @@
 text{*Forwarding lemmas, to aid simplification*}
 
 lemma AuthReq_msg_in_parts_spies:
-     "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;
+     "[|Gets M \<lbrace>P_I, OIData, HPIData\<rbrace> \<in> set evs;
         evs \<in> set_pur|] ==> P_I \<in> parts (knows Spy evs)"
 by auto
 
 lemma AuthReq_msg_in_analz_spies:
-     "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;
+     "[|Gets M \<lbrace>P_I, OIData, HPIData\<rbrace> \<in> set evs;
         evs \<in> set_pur|] ==> P_I \<in> analz (knows Spy evs)"
 by (blast dest: Gets_imp_knows_Spy [THEN analz.Inj])
 
@@ -443,13 +443,13 @@
 subsection{*Public Keys in Certificates are Correct*}
 
 lemma Crypt_valid_pubEK [dest!]:
-     "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
+     "[| Crypt (priSK RCA) \<lbrace>Agent C, Key EKi, onlyEnc\<rbrace>
            \<in> parts (knows Spy evs);
          evs \<in> set_pur |] ==> EKi = pubEK C"
 by (erule rev_mp, erule set_pur.induct, auto)
 
 lemma Crypt_valid_pubSK [dest!]:
-     "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
+     "[| Crypt (priSK RCA) \<lbrace>Agent C, Key SKi, onlySig\<rbrace>
            \<in> parts (knows Spy evs);
          evs \<in> set_pur |] ==> SKi = pubSK C"
 by (erule rev_mp, erule set_pur.induct, auto)
@@ -466,15 +466,15 @@
 by (unfold cert_def signCert_def, auto)
 
 lemma Says_certificate_valid [simp]:
-     "[| Says A B (sign SK {|lid, xid, cc, cm,
-                           cert C EK onlyEnc (priSK RCA)|}) \<in> set evs;
+     "[| Says A B (sign SK \<lbrace>lid, xid, cc, cm,
+                           cert C EK onlyEnc (priSK RCA)\<rbrace>) \<in> set evs;
          evs \<in> set_pur |]
       ==> EK = pubEK C"
 by (unfold sign_def, auto)
 
 lemma Gets_certificate_valid [simp]:
-     "[| Gets A (sign SK {|lid, xid, cc, cm,
-                           cert C EK onlyEnc (priSK RCA)|}) \<in> set evs;
+     "[| Gets A (sign SK \<lbrace>lid, xid, cc, cm,
+                           cert C EK onlyEnc (priSK RCA)\<rbrace>) \<in> set evs;
          evs \<in> set_pur |]
       ==> EK = pubEK C"
 by (frule Gets_imp_Says, auto)
@@ -607,8 +607,8 @@
       ==> 
        (\<exists>V W X Y KC2 M. \<exists>P \<in> bad.
           Says (Cardholder k) M
-               {|{|W, EXcrypt KC2 (pubEK P) X {|Y, Nonce (PANSecret k)|}|},
-                 V|}  \<in>  set evs)"
+               \<lbrace>\<lbrace>W, EXcrypt KC2 (pubEK P) X \<lbrace>Y, Nonce (PANSecret k)\<rbrace>\<rbrace>,
+                 V\<rbrace>  \<in>  set evs)"
 apply (erule rev_mp)
 apply (erule set_pur.induct)
 apply (frule_tac [9] AuthReq_msg_in_analz_spies)
@@ -679,7 +679,7 @@
      "[| Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;
          CardSecret k = 0;  evs \<in> set_pur|]
     ==> \<exists>P M KC1 K X Y.
-     Says C M {|EXHcrypt KC1 (pubEK P) X (Pan (pan C)), Y|}
+     Says C M \<lbrace>EXHcrypt KC1 (pubEK P) X (Pan (pan C)), Y\<rbrace>
           \<in> set evs  &
      P \<in> bad"
 apply (erule rev_mp)
@@ -703,9 +703,9 @@
  "[|Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;
     CardSecret k \<noteq> 0;  evs \<in> set_pur|]
   ==> \<exists>P M KC2 PIDualSign_1 PIDualSign_2 other OIDualSign.
-      Says C M {|{|PIDualSign_1, 
-                   EXcrypt KC2 (pubEK P) PIDualSign_2 {|Pan (pan C), other|}|}, 
-       OIDualSign|} \<in> set evs  &  P \<in> bad"
+      Says C M \<lbrace>\<lbrace>PIDualSign_1, 
+                   EXcrypt KC2 (pubEK P) PIDualSign_2 \<lbrace>Pan (pan C), other\<rbrace>\<rbrace>, 
+       OIDualSign\<rbrace> \<in> set evs  &  P \<in> bad"
 apply (erule rev_mp)
 apply (erule set_pur.induct)
 apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
@@ -730,7 +730,7 @@
 subsection{*Proofs Common to Signed and Unsigned Versions*}
 
 lemma M_Notes_PG:
-     "[|Notes M {|Number LID_M, Agent P, Agent M, Agent C, etc|} \<in> set evs;
+     "[|Notes M \<lbrace>Number LID_M, Agent P, Agent M, Agent C, etc\<rbrace> \<in> set evs;
         evs \<in> set_pur|] ==> \<exists>j. P = PG j"
 by (erule rev_mp, erule set_pur.induct, simp_all)
 
@@ -738,12 +738,12 @@
       (Payment Gateway)*}
 lemma goodM_gives_correct_PG:
      "[| MsgPInitRes = 
-            {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|};
+            \<lbrace>Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)\<rbrace>;
          Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);
          evs \<in> set_pur; M \<notin> bad |]
       ==> \<exists>j trans.
             P = PG j &
-            Notes M {|Number LID_M, Agent P, trans|} \<in> set evs"
+            Notes M \<lbrace>Number LID_M, Agent P, trans\<rbrace> \<in> set evs"
 apply clarify
 apply (erule rev_mp)
 apply (erule set_pur.induct)
@@ -753,23 +753,23 @@
 done
 
 lemma C_gets_correct_PG:
-     "[| Gets A (sign (priSK M) {|Number LID_M, xid, cc, cm,
-                              cert P EKj onlyEnc (priSK RCA)|}) \<in> set evs;
+     "[| Gets A (sign (priSK M) \<lbrace>Number LID_M, xid, cc, cm,
+                              cert P EKj onlyEnc (priSK RCA)\<rbrace>) \<in> set evs;
          evs \<in> set_pur;  M \<notin> bad|]
       ==> \<exists>j trans.
             P = PG j &
-            Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
+            Notes M \<lbrace>Number LID_M, Agent P, trans\<rbrace> \<in> set evs &
             EKj = pubEK P"
 by (rule refl [THEN goodM_gives_correct_PG, THEN exE], auto)
 
 text{*When C receives PInitRes, he learns M's choice of P*}
 lemma C_verifies_PInitRes:
- "[| MsgPInitRes = {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M,
-           cert P EKj onlyEnc (priSK RCA)|};
+ "[| MsgPInitRes = \<lbrace>Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M,
+           cert P EKj onlyEnc (priSK RCA)\<rbrace>;
      Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);
      evs \<in> set_pur;  M \<notin> bad|]
   ==> \<exists>j trans.
-         Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
+         Notes M \<lbrace>Number LID_M, Agent P, trans\<rbrace> \<in> set evs &
          P = PG j &
          EKj = pubEK P"
 apply clarify
@@ -783,12 +783,12 @@
 text{*Corollary of previous one*}
 lemma Says_C_PInitRes:
      "[|Says A C (sign (priSK M)
-                      {|Number LID_M, Number XID,
+                      \<lbrace>Number LID_M, Number XID,
                         Nonce Chall_C, Nonce Chall_M,
-                        cert P EKj onlyEnc (priSK RCA)|})
+                        cert P EKj onlyEnc (priSK RCA)\<rbrace>)
            \<in> set evs;  M \<notin> bad;  evs \<in> set_pur|]
       ==> \<exists>j trans.
-           Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
+           Notes M \<lbrace>Number LID_M, Agent P, trans\<rbrace> \<in> set evs &
            P = PG j &
            EKj = pubEK (PG j)"
 apply (frule Says_certificate_valid)
@@ -800,13 +800,13 @@
 text{*When P receives an AuthReq, he knows that the signed part originated 
       with M. PIRes also has a signed message from M....*}
 lemma P_verifies_AuthReq:
-     "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
-         Crypt (priSK M) (Hash {|AuthReqData, Hash P_I|})
+     "[| AuthReqData = \<lbrace>Number LID_M, Number XID, HOIData, HOD\<rbrace>;
+         Crypt (priSK M) (Hash \<lbrace>AuthReqData, Hash P_I\<rbrace>)
            \<in> parts (knows Spy evs);
          evs \<in> set_pur;  M \<notin> bad|]
       ==> \<exists>j trans KM OIData HPIData.
-            Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
-            Gets M {|P_I, OIData, HPIData|} \<in> set evs &
+            Notes M \<lbrace>Number LID_M, Agent (PG j), trans\<rbrace> \<in> set evs &
+            Gets M \<lbrace>P_I, OIData, HPIData\<rbrace> \<in> set evs &
             Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
               \<in> set evs"
 apply clarify
@@ -825,18 +825,18 @@
   @{term "Crypt K (sign SK M)"} requires assuming @{term K} to be secure, since
   otherwise the Spy could create that message.*}
 theorem M_verifies_AuthRes:
-  "[| MsgAuthRes = {|{|Number LID_M, Number XID, Number PurchAmt|}, 
-                     Hash authCode|};
+  "[| MsgAuthRes = \<lbrace>\<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>, 
+                     Hash authCode\<rbrace>;
       Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs);
       PG j \<notin> bad;  evs \<in> set_pur|]
    ==> \<exists>M KM KP HOIData HOD P_I.
         Gets (PG j)
            (EncB (priSK M) KM (pubEK (PG j))
-                    {|Number LID_M, Number XID, HOIData, HOD|}
+                    \<lbrace>Number LID_M, Number XID, HOIData, HOD\<rbrace>
                     P_I) \<in> set evs &
         Says (PG j) M
              (EncB (priSK (PG j)) KP (pubEK M)
-              {|Number LID_M, Number XID, Number PurchAmt|}
+              \<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>
               authCode) \<in> set evs"
 apply clarify
 apply (erule rev_mp)
@@ -852,12 +852,12 @@
 text{*What we can derive from the ASSUMPTION that C issued a purchase request.
    In the unsigned case, we must trust "C": there's no authentication.*}
 lemma C_determines_EKj:
-     "[| Says C M {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)),
-                    OIData, Hash{|PIHead, Pan (pan C)|} |} \<in> set evs;
-         PIHead = {|Number LID_M, Trans_details|};
+     "[| Says C M \<lbrace>EXHcrypt KC1 EKj \<lbrace>PIHead, Hash OIData\<rbrace> (Pan (pan C)),
+                    OIData, Hash\<lbrace>PIHead, Pan (pan C)\<rbrace> \<rbrace> \<in> set evs;
+         PIHead = \<lbrace>Number LID_M, Trans_details\<rbrace>;
          evs \<in> set_pur;  C = Cardholder k;  M \<notin> bad|]
   ==> \<exists>trans j.
-               Notes M {|Number LID_M, Agent (PG j), trans |} \<in> set evs &
+               Notes M \<lbrace>Number LID_M, Agent (PG j), trans \<rbrace> \<in> set evs &
                EKj = pubEK (PG j)"
 apply clarify
 apply (erule rev_mp)
@@ -870,11 +870,11 @@
 
 text{*Unicity of @{term LID_M} between Merchant and Cardholder notes*}
 lemma unique_LID_M:
-     "[|Notes (Merchant i) {|Number LID_M, Agent P, Trans|} \<in> set evs;
-        Notes C {|Number LID_M, Agent M, Agent C, Number OD,
-             Number PA|} \<in> set evs;
+     "[|Notes (Merchant i) \<lbrace>Number LID_M, Agent P, Trans\<rbrace> \<in> set evs;
+        Notes C \<lbrace>Number LID_M, Agent M, Agent C, Number OD,
+             Number PA\<rbrace> \<in> set evs;
         evs \<in> set_pur|]
-      ==> M = Merchant i & Trans = {|Agent M, Agent C, Number OD, Number PA|}"
+      ==> M = Merchant i & Trans = \<lbrace>Agent M, Agent C, Number OD, Number PA\<rbrace>"
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule set_pur.induct, simp_all)
@@ -883,8 +883,8 @@
 
 text{*Unicity of @{term LID_M}, for two Merchant Notes events*}
 lemma unique_LID_M2:
-     "[|Notes M {|Number LID_M, Trans|} \<in> set evs;
-        Notes M {|Number LID_M, Trans'|} \<in> set evs;
+     "[|Notes M \<lbrace>Number LID_M, Trans\<rbrace> \<in> set evs;
+        Notes M \<lbrace>Number LID_M, Trans'\<rbrace> \<in> set evs;
         evs \<in> set_pur|] ==> Trans' = Trans"
 apply (erule rev_mp)
 apply (erule rev_mp)
@@ -907,7 +907,7 @@
 
 text{*Similar, with nested Hash*}
 lemma signed_Hash_imp_used:
-     "[| Crypt (priSK C) (Hash {|H, Hash X|}) \<in> parts (knows Spy evs);
+     "[| Crypt (priSK C) (Hash \<lbrace>H, Hash X\<rbrace>) \<in> parts (knows Spy evs);
          C \<notin> bad;  evs \<in> set_pur|] ==> parts {X} \<subseteq> used evs"
 apply (erule rev_mp)
 apply (erule set_pur.induct)
@@ -920,7 +920,7 @@
 text{*Lemma needed below: for the case that
   if PRes is present, then @{text LID_M} has been used.*}
 lemma PRes_imp_LID_used:
-     "[| Crypt (priSK M) (Hash {|N, X|}) \<in> parts (knows Spy evs);
+     "[| Crypt (priSK M) (Hash \<lbrace>N, X\<rbrace>) \<in> parts (knows Spy evs);
          M \<notin> bad;  evs \<in> set_pur|] ==> N \<in> used evs"
 by (drule signed_imp_used, auto)
 
@@ -928,16 +928,16 @@
   He also knows that P is the same PG as before*}
 lemma C_verifies_PRes_lemma:
      "[| Crypt (priSK M) (Hash MsgPRes) \<in> parts (knows Spy evs);
-         Notes C {|Number LID_M, Trans |} \<in> set evs;
-         Trans = {| Agent M, Agent C, Number OrderDesc, Number PurchAmt |};
-         MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
-                Hash (Number PurchAmt)|};
+         Notes C \<lbrace>Number LID_M, Trans \<rbrace> \<in> set evs;
+         Trans = \<lbrace> Agent M, Agent C, Number OrderDesc, Number PurchAmt \<rbrace>;
+         MsgPRes = \<lbrace>Number LID_M, Number XID, Nonce Chall_C,
+                Hash (Number PurchAmt)\<rbrace>;
          evs \<in> set_pur;  M \<notin> bad|]
   ==> \<exists>j KP.
-        Notes M {|Number LID_M, Agent (PG j), Trans |}
+        Notes M \<lbrace>Number LID_M, Agent (PG j), Trans \<rbrace>
           \<in> set evs &
         Gets M (EncB (priSK (PG j)) KP (pubEK M)
-                {|Number LID_M, Number XID, Number PurchAmt|}
+                \<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>
                 authCode)
           \<in> set evs &
         Says M C (sign (priSK M) MsgPRes) \<in> set evs"
@@ -958,16 +958,16 @@
 Merchant, he knows that M sent it. He also knows that M received a message signed
 by a Payment Gateway chosen by M to authorize the purchase.*}
 theorem C_verifies_PRes:
-     "[| MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
-                     Hash (Number PurchAmt)|};
+     "[| MsgPRes = \<lbrace>Number LID_M, Number XID, Nonce Chall_C,
+                     Hash (Number PurchAmt)\<rbrace>;
          Gets C (sign (priSK M) MsgPRes) \<in> set evs;
-         Notes C {|Number LID_M, Agent M, Agent C, Number OrderDesc,
-                   Number PurchAmt|} \<in> set evs;
+         Notes C \<lbrace>Number LID_M, Agent M, Agent C, Number OrderDesc,
+                   Number PurchAmt\<rbrace> \<in> set evs;
          evs \<in> set_pur;  M \<notin> bad|]
   ==> \<exists>P KP trans.
-        Notes M {|Number LID_M,Agent P, trans|} \<in> set evs &
+        Notes M \<lbrace>Number LID_M,Agent P, trans\<rbrace> \<in> set evs &
         Gets M (EncB (priSK P) KP (pubEK M)
-                {|Number LID_M, Number XID, Number PurchAmt|}
+                \<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>
                 authCode)  \<in>  set evs &
         Says M C (sign (priSK M) MsgPRes) \<in> set evs"
 apply (rule C_verifies_PRes_lemma [THEN exE])
@@ -979,17 +979,17 @@
 text{*Some Useful Lemmas: the cardholder knows what he is doing*}
 
 lemma Crypt_imp_Says_Cardholder:
-     "[| Crypt K {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|}
+     "[| Crypt K \<lbrace>\<lbrace>\<lbrace>Number LID_M, others\<rbrace>, Hash OIData\<rbrace>, Hash PANData\<rbrace>
            \<in> parts (knows Spy evs);
-         PANData = {|Pan (pan (Cardholder k)), Nonce (PANSecret k)|};
+         PANData = \<lbrace>Pan (pan (Cardholder k)), Nonce (PANSecret k)\<rbrace>;
          Key K \<notin> analz (knows Spy evs);
          evs \<in> set_pur|]
   ==> \<exists>M shash EK HPIData.
-       Says (Cardholder k) M {|{|shash,
+       Says (Cardholder k) M \<lbrace>\<lbrace>shash,
           Crypt K
-            {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|},
-           Crypt EK {|Key K, PANData|}|},
-          OIData, HPIData|} \<in> set evs"
+            \<lbrace>\<lbrace>\<lbrace>Number LID_M, others\<rbrace>, Hash OIData\<rbrace>, Hash PANData\<rbrace>,
+           Crypt EK \<lbrace>Key K, PANData\<rbrace>\<rbrace>,
+          OIData, HPIData\<rbrace> \<in> set evs"
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule rev_mp)
@@ -1000,15 +1000,15 @@
 done
 
 lemma Says_PReqS_imp_trans_details_C:
-     "[| MsgPReqS = {|{|shash,
+     "[| MsgPReqS = \<lbrace>\<lbrace>shash,
                  Crypt K
-                  {|{|{|Number LID_M, PIrest|}, Hash OIData|}, hashpd|},
-            cryptek|}, data|};
+                  \<lbrace>\<lbrace>\<lbrace>Number LID_M, PIrest\<rbrace>, Hash OIData\<rbrace>, hashpd\<rbrace>,
+            cryptek\<rbrace>, data\<rbrace>;
          Says (Cardholder k) M MsgPReqS \<in> set evs;
          evs \<in> set_pur |]
    ==> \<exists>trans.
            Notes (Cardholder k) 
-                 {|Number LID_M, Agent M, Agent (Cardholder k), trans|}
+                 \<lbrace>Number LID_M, Agent M, Agent (Cardholder k), trans\<rbrace>
             \<in> set evs"
 apply (erule rev_mp)
 apply (erule rev_mp)
@@ -1020,7 +1020,7 @@
 text{*Can't happen: only Merchants create this type of Note*}
 lemma Notes_Cardholder_self_False:
      "[|Notes (Cardholder k)
-          {|Number n, Agent P, Agent (Cardholder k), Agent C, etc|} \<in> set evs;
+          \<lbrace>Number n, Agent P, Agent (Cardholder k), Agent C, etc\<rbrace> \<in> set evs;
         evs \<in> set_pur|] ==> False"
 by (erule rev_mp, erule set_pur.induct, auto)
 
@@ -1028,14 +1028,14 @@
   Using XID he knows it was intended for him.
   This guarantee isn't useful to P, who never gets OIData.*}
 theorem M_verifies_Signed_PReq:
- "[| MsgDualSign = {|HPIData, Hash OIData|};
-     OIData = {|Number LID_M, etc|};
+ "[| MsgDualSign = \<lbrace>HPIData, Hash OIData\<rbrace>;
+     OIData = \<lbrace>Number LID_M, etc\<rbrace>;
      Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
-     Notes M {|Number LID_M, Agent P, extras|} \<in> set evs;
+     Notes M \<lbrace>Number LID_M, Agent P, extras\<rbrace> \<in> set evs;
      M = Merchant i;  C = Cardholder k;  C \<notin> bad;  evs \<in> set_pur|]
   ==> \<exists>PIData PICrypt.
         HPIData = Hash PIData &
-        Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|}
+        Says C M \<lbrace>\<lbrace>sign (priSK C) MsgDualSign, PICrypt\<rbrace>, OIData, Hash PIData\<rbrace>
           \<in> set evs"
 apply clarify
 apply (erule rev_mp)
@@ -1054,20 +1054,20 @@
   PIData. I don't see how to link @{term "PG j"} and @{text LID_M} without
   assuming @{term "M \<notin> bad"}.*}
 theorem P_verifies_Signed_PReq:
-     "[| MsgDualSign = {|Hash PIData, HOIData|};
-         PIData = {|PIHead, PANData|};
-         PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
-                    TransStain|};
+     "[| MsgDualSign = \<lbrace>Hash PIData, HOIData\<rbrace>;
+         PIData = \<lbrace>PIHead, PANData\<rbrace>;
+         PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+                    TransStain\<rbrace>;
          Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
          evs \<in> set_pur;  C \<notin> bad;  M \<notin> bad|]
     ==> \<exists>OIData OrderDesc K j trans.
-          HOD = Hash{|Number OrderDesc, Number PurchAmt|} &
+          HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace> &
           HOIData = Hash OIData &
-          Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
-          Says C M {|{|sign (priSK C) MsgDualSign,
+          Notes M \<lbrace>Number LID_M, Agent (PG j), trans\<rbrace> \<in> set evs &
+          Says C M \<lbrace>\<lbrace>sign (priSK C) MsgDualSign,
                      EXcrypt K (pubEK (PG j))
-                                {|PIHead, Hash OIData|} PANData|},
-                     OIData, Hash PIData|}
+                                \<lbrace>PIHead, Hash OIData\<rbrace> PANData\<rbrace>,
+                     OIData, Hash PIData\<rbrace>
             \<in> set evs"
 apply clarify
 apply (erule rev_mp)
@@ -1076,12 +1076,12 @@
 done
 
 lemma C_determines_EKj_signed:
-     "[| Says C M {|{|sign (priSK C) text,
-                      EXcrypt K EKj {|PIHead, X|} Y|}, Z|} \<in> set evs;
-         PIHead = {|Number LID_M, Number XID, W|};
+     "[| Says C M \<lbrace>\<lbrace>sign (priSK C) text,
+                      EXcrypt K EKj \<lbrace>PIHead, X\<rbrace> Y\<rbrace>, Z\<rbrace> \<in> set evs;
+         PIHead = \<lbrace>Number LID_M, Number XID, W\<rbrace>;
          C = Cardholder k;  evs \<in> set_pur;  M \<notin> bad|]
   ==> \<exists> trans j.
-         Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
+         Notes M \<lbrace>Number LID_M, Agent (PG j), trans\<rbrace> \<in> set evs &
          EKj = pubEK (PG j)"
 apply clarify
 apply (erule rev_mp)
@@ -1090,11 +1090,11 @@
 done
 
 lemma M_Says_AuthReq:
-     "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
-         sign (priSK M) {|AuthReqData, Hash P_I|} \<in> parts (knows Spy evs);
+     "[| AuthReqData = \<lbrace>Number LID_M, Number XID, HOIData, HOD\<rbrace>;
+         sign (priSK M) \<lbrace>AuthReqData, Hash P_I\<rbrace> \<in> parts (knows Spy evs);
          evs \<in> set_pur;  M \<notin> bad|]
    ==> \<exists>j trans KM.
-           Notes M {|Number LID_M, Agent (PG j), trans |} \<in> set evs &
+           Notes M \<lbrace>Number LID_M, Agent (PG j), trans \<rbrace> \<in> set evs &
              Says M (PG j)
                (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
               \<in> set evs"
@@ -1106,17 +1106,17 @@
   Even here we cannot be certain about what C sent to M, since a bad
   PG could have replaced the two key fields.  (NOT USED)*}
 lemma Signed_PReq_imp_Says_Cardholder:
-     "[| MsgDualSign = {|Hash PIData, Hash OIData|};
-         OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, etc|};
-         PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
-                    TransStain|};
-         PIData = {|PIHead, PANData|};
+     "[| MsgDualSign = \<lbrace>Hash PIData, Hash OIData\<rbrace>;
+         OIData = \<lbrace>Number LID_M, Number XID, Nonce Chall_C, HOD, etc\<rbrace>;
+         PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+                    TransStain\<rbrace>;
+         PIData = \<lbrace>PIHead, PANData\<rbrace>;
          Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
          M = Merchant i;  C = Cardholder k;  C \<notin> bad;  evs \<in> set_pur|]
       ==> \<exists>KC EKj.
-            Says C M {|{|sign (priSK C) MsgDualSign,
-                       EXcrypt KC EKj {|PIHead, Hash OIData|} PANData|},
-                       OIData, Hash PIData|}
+            Says C M \<lbrace>\<lbrace>sign (priSK C) MsgDualSign,
+                       EXcrypt KC EKj \<lbrace>PIHead, Hash OIData\<rbrace> PANData\<rbrace>,
+                       OIData, Hash PIData\<rbrace>
               \<in> set evs"
 apply clarify
 apply hypsubst_thin
@@ -1128,7 +1128,7 @@
 text{*When P receives an AuthReq and a dual signature, he knows that C and M
   agree on the essential details.  PurchAmt however is never sent by M to
   P; instead C and M both send 
-     @{term "HOD = Hash{|Number OrderDesc, Number PurchAmt|}"}
+     @{term "HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace>"}
   and P compares the two copies of HOD.
 
   Agreement can't be proved for some things, including the symmetric keys
@@ -1137,30 +1137,30 @@
   the EXcrypt involves the correct PG's key.
 *}
 theorem P_sees_CM_agreement:
-     "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
+     "[| AuthReqData = \<lbrace>Number LID_M, Number XID, HOIData, HOD\<rbrace>;
          KC \<in> symKeys;
          Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
            \<in> set evs;
          C = Cardholder k;
-         PI_sign = sign (priSK C) {|Hash PIData, HOIData|};
-         P_I = {|PI_sign,
-                 EXcrypt KC (pubEK (PG j)) {|PIHead, HOIData|} PANData|};
-         PANData = {|Pan (pan C), Nonce (PANSecret k)|};
-         PIData = {|PIHead, PANData|};
-         PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
-                    TransStain|};
+         PI_sign = sign (priSK C) \<lbrace>Hash PIData, HOIData\<rbrace>;
+         P_I = \<lbrace>PI_sign,
+                 EXcrypt KC (pubEK (PG j)) \<lbrace>PIHead, HOIData\<rbrace> PANData\<rbrace>;
+         PANData = \<lbrace>Pan (pan C), Nonce (PANSecret k)\<rbrace>;
+         PIData = \<lbrace>PIHead, PANData\<rbrace>;
+         PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
+                    TransStain\<rbrace>;
          evs \<in> set_pur;  C \<notin> bad;  M \<notin> bad|]
   ==> \<exists>OIData OrderDesc KM' trans j' KC' KC'' P_I' P_I''.
-           HOD = Hash{|Number OrderDesc, Number PurchAmt|} &
+           HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace> &
            HOIData = Hash OIData &
-           Notes M {|Number LID_M, Agent (PG j'), trans|} \<in> set evs &
-           Says C M {|P_I', OIData, Hash PIData|} \<in> set evs &
+           Notes M \<lbrace>Number LID_M, Agent (PG j'), trans\<rbrace> \<in> set evs &
+           Says C M \<lbrace>P_I', OIData, Hash PIData\<rbrace> \<in> set evs &
            Says M (PG j') (EncB (priSK M) KM' (pubEK (PG j'))
                            AuthReqData P_I'')  \<in>  set evs &
-           P_I' = {|PI_sign,
-             EXcrypt KC' (pubEK (PG j')) {|PIHead, Hash OIData|} PANData|} &
-           P_I'' = {|PI_sign,
-             EXcrypt KC'' (pubEK (PG j)) {|PIHead, Hash OIData|} PANData|}"
+           P_I' = \<lbrace>PI_sign,
+             EXcrypt KC' (pubEK (PG j')) \<lbrace>PIHead, Hash OIData\<rbrace> PANData\<rbrace> &
+           P_I'' = \<lbrace>PI_sign,
+             EXcrypt KC'' (pubEK (PG j)) \<lbrace>PIHead, Hash OIData\<rbrace> PANData\<rbrace>"
 apply clarify
 apply (rule exE)
 apply (rule P_verifies_Signed_PReq [OF refl refl refl])