diff -r b38a54bbfbd6 -r 9576b510f6a2 src/CCL/ex/Flag.thy
--- a/src/CCL/ex/Flag.thy	Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/ex/Flag.thy	Tue Nov 11 15:55:31 2014 +0100
@@ -22,32 +22,32 @@
 definition blue :: "i"
   where "blue == inr(inr(one))"
 
-definition ccase :: "[i,i,i,i]=>i"
-  where "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))"
+definition ccase :: "[i,i,i,i]\<Rightarrow>i"
+  where "ccase(c,r,w,b) == when(c, \<lambda>x. r, \<lambda>wb. when(wb, \<lambda>x. w, \<lambda>x. b))"
 
 definition flag :: "i"
   where
     "flag == lam l. letrec
       flagx l be lcase(l,<[],<[],[]>>,
-                       %h t. split(flagx(t),%lr p. split(p,%lw lb.
+                       \<lambda>h t. split(flagx(t), \<lambda>lr p. split(p, \<lambda>lw lb.
                             ccase(h, <red$lr,<lw,lb>>,
                                      <lr,<white$lw,lb>>,
                                      <lr,<lw,blue$lb>>))))
       in flagx(l)"
 
-axiomatization Perm :: "i => i => o"
-definition Flag :: "i => i => o" where
+axiomatization Perm :: "i \<Rightarrow> i \<Rightarrow> o"
+definition Flag :: "i \<Rightarrow> i \<Rightarrow> o" where
   "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour).
-                x = <lr,<lw,lb>> -->
-              (ALL c:Colour.(c mem lr = true --> c=red) &
-                            (c mem lw = true --> c=white) &
-                            (c mem lb = true --> c=blue)) &
+                x = <lr,<lw,lb>> \<longrightarrow>
+              (ALL c:Colour.(c mem lr = true \<longrightarrow> c=red) \<and>
+                            (c mem lw = true \<longrightarrow> c=white) \<and>
+                            (c mem lb = true \<longrightarrow> c=blue)) \<and>
               Perm(l,lr @ lw @ lb)"
 
 
 lemmas flag_defs = Colour_def red_def white_def blue_def ccase_def
 
-lemma ColourXH: "a : Colour <-> (a=red | a=white | a=blue)"
+lemma ColourXH: "a : Colour \<longleftrightarrow> (a=red | a=white | a=blue)"
   unfolding simp_type_defs flag_defs by blast
 
 lemma redT: "red : Colour"
@@ -56,8 +56,8 @@
   unfolding ColourXH by blast+
 
 lemma ccaseT:
-  "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |]
-    ==> ccase(c,r,w,b) : C(c)"
+  "\<lbrakk>c:Colour; c=red \<Longrightarrow> r : C(red); c=white \<Longrightarrow> w : C(white); c=blue \<Longrightarrow> b : C(blue)\<rbrakk>
+    \<Longrightarrow> ccase(c,r,w,b) : C(c)"
   unfolding flag_defs by ncanT
 
 lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)"