diff -r e96292f32c3c -r 38b73f7940af src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Message.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -48,21 +48,17 @@
          | Crypt  key msg   \<comment>\<open>Encryption, public- or shared-key\<close>
 
 
-text\<open>Concrete syntax: messages appear as {|A,B,NA|}, etc...\<close>
+text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
 syntax
-  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
-
-syntax (xsymbols)
-  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
-
+  "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
 translations
-  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
-  "{|x, y|}"      == "CONST MPair x y"
+  "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+  "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
 
 
 definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
     \<comment>\<open>Message Y paired with a MAC computed with the help of X\<close>
-    "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
+    "Hash[X] Y == \<lbrace>Hash\<lbrace>X,Y\<rbrace>, Y\<rbrace>"
 
 definition keysFor :: "msg set => key set" where
     \<comment>\<open>Keys useful to decrypt elements of a message set\<close>
@@ -75,9 +71,9 @@
   parts :: "msg set => msg set"
   for H :: "msg set"
   where
-    Inj [intro]:               "X \<in> H ==> X \<in> parts H"
-  | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
-  | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
+    Inj [intro]: "X \<in> H ==> X \<in> parts H"
+  | Fst:         "\<lbrace>X,Y\<rbrace> \<in> parts H ==> X \<in> parts H"
+  | Snd:         "\<lbrace>X,Y\<rbrace> \<in> parts H ==> Y \<in> parts H"
   | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
 
 
@@ -136,7 +132,7 @@
 lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
 by (unfold keysFor_def, auto)
 
-lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
+lemma keysFor_insert_MPair [simp]: "keysFor (insert \<lbrace>X,Y\<rbrace> H) = keysFor H"
 by (unfold keysFor_def, auto)
 
 lemma keysFor_insert_Crypt [simp]: 
@@ -153,7 +149,7 @@
 subsection\<open>Inductive relation "parts"\<close>
 
 lemma MPair_parts:
-     "[| {|X,Y|} \<in> parts H;        
+     "[| \<lbrace>X,Y\<rbrace> \<in> parts H;        
          [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
 by (blast dest: parts.Fst parts.Snd) 
 
@@ -294,8 +290,8 @@
 done
 
 lemma parts_insert_MPair [simp]:
-     "parts (insert {|X,Y|} H) =  
-          insert {|X,Y|} (parts (insert X (insert Y H)))"
+     "parts (insert \<lbrace>X,Y\<rbrace> H) =  
+          insert \<lbrace>X,Y\<rbrace> (parts (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct, auto)
@@ -330,9 +326,9 @@
   analz :: "msg set => msg set"
   for H :: "msg set"
   where
-    Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
-  | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
-  | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
+    Inj [intro,simp]: "X \<in> H ==> X \<in> analz H"
+  | Fst:     "\<lbrace>X,Y\<rbrace> \<in> analz H ==> X \<in> analz H"
+  | Snd:     "\<lbrace>X,Y\<rbrace> \<in> analz H ==> Y \<in> analz H"
   | Decrypt [dest]: 
              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
 
@@ -346,7 +342,7 @@
 
 text\<open>Making it safe speeds up proofs\<close>
 lemma MPair_analz [elim!]:
-     "[| {|X,Y|} \<in> analz H;        
+     "[| \<lbrace>X,Y\<rbrace> \<in> analz H;        
              [| X \<in> analz H; Y \<in> analz H |] ==> P   
           |] ==> P"
 by (blast dest: analz.Fst analz.Snd)
@@ -427,8 +423,8 @@
 done
 
 lemma analz_insert_MPair [simp]:
-     "analz (insert {|X,Y|} H) =  
-          insert {|X,Y|} (analz (insert X (insert Y H)))"
+     "analz (insert \<lbrace>X,Y\<rbrace> H) =  
+          insert \<lbrace>X,Y\<rbrace> (analz (insert X (insert Y H)))"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule analz.induct, auto)
@@ -540,7 +536,7 @@
 
 text\<open>If there are no pairs or encryptions then analz does nothing\<close>
 lemma analz_trivial:
-     "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
+     "[| \<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
 apply safe
 apply (erule analz.induct, blast+)
 done
@@ -571,7 +567,7 @@
   | Agent  [intro]:   "Agent agt \<in> synth H"
   | Number [intro]:   "Number n  \<in> synth H"
   | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
-  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
+  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> \<lbrace>X,Y\<rbrace> \<in> synth H"
   | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
 
 text\<open>Monotonicity\<close>
@@ -585,7 +581,7 @@
  "Nonce n \<in> synth H"
  "Key K \<in> synth H"
  "Hash X \<in> synth H"
- "{|X,Y|} \<in> synth H"
+ "\<lbrace>X,Y\<rbrace> \<in> synth H"
  "Crypt K X \<in> synth H"
 
 lemma synth_increasing: "H \<subseteq> synth(H)"
@@ -694,7 +690,7 @@
 text\<open>Without this equation, other rules for synth and analz would yield
   redundant cases\<close>
 lemma MPair_synth_analz [iff]:
-     "({|X,Y|} \<in> synth (analz H)) =  
+     "(\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) =  
       (X \<in> synth (analz H) & Y \<in> synth (analz H))"
 by blast
 
@@ -706,7 +702,7 @@
 
 lemma Hash_synth_analz [simp]:
      "X \<notin> synth (analz H)  
-      ==> (Hash{|X,Y|} \<in> synth (analz H)) = (Hash{|X,Y|} \<in> analz H)"
+      ==> (Hash\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) = (Hash\<lbrace>X,Y\<rbrace> \<in> analz H)"
 by blast
 
 
@@ -742,11 +738,11 @@
 by (simp add: HPair_def)
 
 lemma MPair_eq_HPair [iff]:
-     "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
+     "(\<lbrace>X',Y'\<rbrace> = Hash[X] Y) = (X' = Hash\<lbrace>X,Y\<rbrace> & Y'=Y)"
 by (simp add: HPair_def)
 
 lemma HPair_eq_MPair [iff]:
-     "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
+     "(Hash[X] Y = \<lbrace>X',Y'\<rbrace>) = (X' = Hash\<lbrace>X,Y\<rbrace> & Y'=Y)"
 by (auto simp add: HPair_def)
 
 
@@ -757,18 +753,18 @@
 
 lemma parts_insert_HPair [simp]: 
     "parts (insert (Hash[X] Y) H) =  
-     insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"
+     insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (parts (insert Y H)))"
 by (simp add: HPair_def)
 
 lemma analz_insert_HPair [simp]: 
     "analz (insert (Hash[X] Y) H) =  
-     insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"
+     insert (Hash[X] Y) (insert (Hash\<lbrace>X,Y\<rbrace>) (analz (insert Y H)))"
 by (simp add: HPair_def)
 
 lemma HPair_synth_analz [simp]:
      "X \<notin> synth (analz H)  
     ==> (Hash[X] Y \<in> synth (analz H)) =  
-        (Hash {|X, Y|} \<in> analz H & Y \<in> synth (analz H))"
+        (Hash \<lbrace>X, Y\<rbrace> \<in> analz H & Y \<in> synth (analz H))"
 by (auto simp add: HPair_def)
 
 
@@ -814,14 +810,14 @@
   | Number: "Number N \<in> keyfree"
   | Nonce:  "Nonce N \<in> keyfree"
   | Hash:   "Hash X \<in> keyfree"
-  | MPair:  "[|X \<in> keyfree;  Y \<in> keyfree|] ==> {|X,Y|} \<in> keyfree"
+  | MPair:  "[|X \<in> keyfree;  Y \<in> keyfree|] ==> \<lbrace>X,Y\<rbrace> \<in> keyfree"
   | Crypt:  "[|X \<in> keyfree|] ==> Crypt K X \<in> keyfree"
 
 
 declare keyfree.intros [intro] 
 
 inductive_cases keyfree_KeyE: "Key K \<in> keyfree"
-inductive_cases keyfree_MPairE: "{|X,Y|} \<in> keyfree"
+inductive_cases keyfree_MPairE: "\<lbrace>X,Y\<rbrace> \<in> keyfree"
 inductive_cases keyfree_CryptE: "Crypt K X \<in> keyfree"
 
 lemma parts_keyfree: "parts (keyfree) \<subseteq> keyfree"