# HG changeset patch
# User wenzelm
# Date 1546546552 -3600
# Node ID 53982d5ec0bb8a9d8e450876869f5d58daf980be
# Parent  9171d1ce5a355615d3d32124b4f066d6b3f24fab
isabelle update -u mixfix_cartouches;

diff -r 9171d1ce5a35 -r 53982d5ec0bb src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/FOL/IFOL.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -31,13 +31,13 @@
 typedecl o
 
 judgment
-  Trueprop :: "o \<Rightarrow> prop"  ("(_)" 5)
+  Trueprop :: "o \<Rightarrow> prop"  (\<open>(_)\<close> 5)
 
 
 subsubsection \<open>Equality\<close>
 
 axiomatization
-  eq :: "['a, 'a] \<Rightarrow> o"  (infixl "=" 50)
+  eq :: "['a, 'a] \<Rightarrow> o"  (infixl \<open>=\<close> 50)
 where
   refl: "a = a" and
   subst: "a = b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
@@ -47,9 +47,9 @@
 
 axiomatization
   False :: o and
-  conj :: "[o, o] => o"  (infixr "\<and>" 35) and
-  disj :: "[o, o] => o"  (infixr "\<or>" 30) and
-  imp :: "[o, o] => o"  (infixr "\<longrightarrow>" 25)
+  conj :: "[o, o] => o"  (infixr \<open>\<and>\<close> 35) and
+  disj :: "[o, o] => o"  (infixr \<open>\<or>\<close> 30) and
+  imp :: "[o, o] => o"  (infixr \<open>\<longrightarrow>\<close> 25)
 where
   conjI: "\<lbrakk>P;  Q\<rbrakk> \<Longrightarrow> P \<and> Q" and
   conjunct1: "P \<and> Q \<Longrightarrow> P" and
@@ -68,8 +68,8 @@
 subsubsection \<open>Quantifiers\<close>
 
 axiomatization
-  All :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10) and
-  Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
+  All :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder \<open>\<forall>\<close> 10) and
+  Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder \<open>\<exists>\<close> 10)
 where
   allI: "(\<And>x. P(x)) \<Longrightarrow> (\<forall>x. P(x))" and
   spec: "(\<forall>x. P(x)) \<Longrightarrow> P(x)" and
@@ -81,35 +81,35 @@
 
 definition "True \<equiv> False \<longrightarrow> False"
 
-definition Not ("\<not> _" [40] 40)
+definition Not (\<open>\<not> _\<close> [40] 40)
   where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
 
-definition iff  (infixr "\<longleftrightarrow>" 25)
+definition iff  (infixr \<open>\<longleftrightarrow>\<close> 25)
   where "P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)"
 
-definition Ex1 :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>!" 10)
+definition Ex1 :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder \<open>\<exists>!\<close> 10)
   where ex1_def: "\<exists>!x. P(x) \<equiv> \<exists>x. P(x) \<and> (\<forall>y. P(y) \<longrightarrow> y = x)"
 
 axiomatization where  \<comment> \<open>Reflection, admissible\<close>
   eq_reflection: "(x = y) \<Longrightarrow> (x \<equiv> y)" and
   iff_reflection: "(P \<longleftrightarrow> Q) \<Longrightarrow> (P \<equiv> Q)"
 
-abbreviation not_equal :: "['a, 'a] \<Rightarrow> o"  (infixl "\<noteq>" 50)
+abbreviation not_equal :: "['a, 'a] \<Rightarrow> o"  (infixl \<open>\<noteq>\<close> 50)
   where "x \<noteq> y \<equiv> \<not> (x = y)"
 
 
 subsubsection \<open>Old-style ASCII syntax\<close>
 
 notation (ASCII)
-  not_equal  (infixl "~=" 50) and
-  Not  ("~ _" [40] 40) and
-  conj  (infixr "&" 35) and
-  disj  (infixr "|" 30) and
-  All  (binder "ALL " 10) and
-  Ex  (binder "EX " 10) and
-  Ex1  (binder "EX! " 10) and
-  imp  (infixr "-->" 25) and
-  iff  (infixr "<->" 25)
+  not_equal  (infixl \<open>~=\<close> 50) and
+  Not  (\<open>~ _\<close> [40] 40) and
+  conj  (infixr \<open>&\<close> 35) and
+  disj  (infixr \<open>|\<close> 30) and
+  All  (binder \<open>ALL \<close> 10) and
+  Ex  (binder \<open>EX \<close> 10) and
+  Ex1  (binder \<open>EX! \<close> 10) and
+  imp  (infixr \<open>-->\<close> 25) and
+  iff  (infixr \<open><->\<close> 25)
 
 
 subsection \<open>Lemmas and proof tools\<close>
@@ -764,10 +764,10 @@
   where "Let(s, f) \<equiv> f(s)"
 
 syntax
-  "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
-  ""            :: "letbind => letbinds"              ("_")
-  "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
-  "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
+  "_bind"       :: "[pttrn, 'a] => letbind"           (\<open>(2_ =/ _)\<close> 10)
+  ""            :: "letbind => letbinds"              (\<open>_\<close>)
+  "_binds"      :: "[letbind, letbinds] => letbinds"  (\<open>_;/ _\<close>)
+  "_Let"        :: "[letbinds, 'a] => 'a"             (\<open>(let (_)/ in (_))\<close> 10)
 
 translations
   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -11,9 +11,9 @@
 typedecl int
 instance int :: "term" ..
 
-consts plus :: "int => int => int" (infixl "+" 60)
-  zero :: int ("0")
-  minus :: "int => int" ("- _")
+consts plus :: "int => int => int" (infixl \<open>+\<close> 60)
+  zero :: int (\<open>0\<close>)
+  minus :: "int => int" (\<open>- _\<close>)
 
 axiomatization where
   int_assoc: "(x + y::int) + z = x + (y + z)" and
@@ -34,17 +34,17 @@
   Fails, cannot generalise parameter.
 *)
 
-locale param3 = fixes p (infix ".." 50)
+locale param3 = fixes p (infix \<open>..\<close> 50)
 print_locale! param3
 
-locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50)
+locale param4 = fixes p :: "'a => 'a => 'a" (infix \<open>..\<close> 50)
 print_locale! param4
 
 
 subsection \<open>Incremental type constraints\<close>
 
 locale constraint1 =
-  fixes  prod (infixl "**" 65)
+  fixes  prod (infixl \<open>**\<close> 65)
   assumes l_id: "x ** y = x"
   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
 print_locale! constraint1
@@ -58,7 +58,7 @@
 section \<open>Inheritance\<close>
 
 locale semi =
-  fixes prod (infixl "**" 65)
+  fixes prod (infixl \<open>**\<close> 65)
   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
 print_locale! semi thm semi_def
 
@@ -68,13 +68,13 @@
     and linv: "inv(x) ** x = one"
 print_locale! lgrp thm lgrp_def lgrp_axioms_def
 
-locale add_lgrp = semi "(++)" for sum (infixl "++" 60) +
+locale add_lgrp = semi "(++)" for sum (infixl \<open>++\<close> 60) +
   fixes zero and neg
   assumes lzero: "zero ++ x = x"
     and lneg: "neg(x) ++ x = zero"
 print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def
 
-locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60)
+locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl \<open>++\<close> 60)
 print_locale! rev_lgrp thm rev_lgrp_def
 
 locale hom = f: semi f + g: semi g for f and g
@@ -94,13 +94,13 @@
 section \<open>Syntax declarations\<close>
 
 locale logic =
-  fixes land (infixl "&&" 55)
-    and lnot ("-- _" [60] 60)
+  fixes land (infixl \<open>&&\<close> 55)
+    and lnot (\<open>-- _\<close> [60] 60)
   assumes assoc: "(x && y) && z = x && (y && z)"
     and notnot: "-- (-- x) = x"
 begin
 
-definition lor (infixl "||" 50) where
+definition lor (infixl \<open>||\<close> 50) where
   "x || y = --(-- x && -- y)"
 
 end
@@ -147,8 +147,8 @@
     and p2 :: "'b => o"
 begin
 
-definition d1 :: "'a => o" ("D1'(_')") where "d1(x) \<longleftrightarrow> \<not> p2(p1(x))"
-definition d2 :: "'b => o" ("D2'(_')") where "d2(x) \<longleftrightarrow> \<not> p2(x)"
+definition d1 :: "'a => o" (\<open>D1'(_')\<close>) where "d1(x) \<longleftrightarrow> \<not> p2(p1(x))"
+definition d2 :: "'b => o" (\<open>D2'(_')\<close>) where "d2(x) \<longleftrightarrow> \<not> p2(x)"
 
 thm d1_def d2_def
 
@@ -191,9 +191,9 @@
 section \<open>Defines\<close>
 
 locale logic_def =
-  fixes land (infixl "&&" 55)
-    and lor (infixl "||" 50)
-    and lnot ("-- _" [60] 60)
+  fixes land (infixl \<open>&&\<close> 55)
+    and lor (infixl \<open>||\<close> 50)
+    and lnot (\<open>-- _\<close> [60] 60)
   assumes assoc: "(x && y) && z = x && (y && z)"
     and notnot: "-- (-- x) = x"
   defines "x || y == --(-- x && -- y)"
@@ -353,7 +353,7 @@
 (* Duality *)
 
 locale order =
-  fixes less :: "'a => 'a => o" (infix "<<" 50)
+  fixes less :: "'a => 'a => o" (infix \<open><<\<close> 50)
   assumes refl: "x << x"
     and trans: "[| x << y; y << z |] ==> x << z"
 
@@ -364,14 +364,14 @@
 print_locale! order  (* Only two instances of order. *)
 
 locale order' =
-  fixes less :: "'a => 'a => o" (infix "<<" 50)
+  fixes less :: "'a => 'a => o" (infix \<open><<\<close> 50)
   assumes refl: "x << x"
     and trans: "[| x << y; y << z |] ==> x << z"
 
 locale order_with_def = order'
 begin
 
-definition greater :: "'a => 'a => o" (infix ">>" 50) where
+definition greater :: "'a => 'a => o" (infix \<open>>>\<close> 50) where
   "x >> y \<longleftrightarrow> y << x"
 
 end
@@ -464,13 +464,13 @@
   by unfold_locales (rule int_assoc int_minus2)+
 
 locale logic2 =
-  fixes land (infixl "&&" 55)
-    and lnot ("-- _" [60] 60)
+  fixes land (infixl \<open>&&\<close> 55)
+    and lnot (\<open>-- _\<close> [60] 60)
   assumes assoc: "(x && y) && z = x && (y && z)"
     and notnot: "-- (-- x) = x"
 begin
 
-definition lor (infixl "||" 50) where
+definition lor (infixl \<open>||\<close> 50) where
   "x || y = --(-- x && -- y)"
 
 end
@@ -495,13 +495,13 @@
 subsection \<open>Rewrite morphism\<close>
 
 locale logic_o =
-  fixes land (infixl "&&" 55)
-    and lnot ("-- _" [60] 60)
+  fixes land (infixl \<open>&&\<close> 55)
+    and lnot (\<open>-- _\<close> [60] 60)
   assumes assoc_o: "(x && y) && z \<longleftrightarrow> x && (y && z)"
     and notnot_o: "-- (-- x) \<longleftrightarrow> x"
 begin
 
-definition lor_o (infixl "||" 50) where
+definition lor_o (infixl \<open>||\<close> 50) where
   "x || y \<longleftrightarrow> --(-- x && -- y)"
 
 end
@@ -536,11 +536,11 @@
 subsection \<open>Inheritance of rewrite morphisms\<close>
 
 locale reflexive =
-  fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
+  fixes le :: "'a => 'a => o" (infix \<open>\<sqsubseteq>\<close> 50)
   assumes refl: "x \<sqsubseteq> x"
 begin
 
-definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
+definition less (infix \<open>\<sqsubset>\<close> 50) where "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
 
 end
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/FOL/ex/Nat.thy
--- a/src/FOL/ex/Nat.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/FOL/ex/Nat.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -13,7 +13,7 @@
 instance nat :: "term" ..
 
 axiomatization
-  Zero :: nat  ("0") and
+  Zero :: nat  (\<open>0\<close>) and
   Suc :: "nat => nat" and
   rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
 where
@@ -23,7 +23,7 @@
   rec_0: "rec(0,a,f) = a" and
   rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
 
-definition add :: "[nat, nat] => nat"  (infixl "+" 60)
+definition add :: "[nat, nat] => nat"  (infixl \<open>+\<close> 60)
   where "m + n == rec(m, n, %x y. Suc(y))"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/FOL/ex/Natural_Numbers.thy
--- a/src/FOL/ex/Natural_Numbers.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/FOL/ex/Natural_Numbers.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -17,7 +17,7 @@
 instance nat :: "term" ..
 
 axiomatization
-  Zero :: nat    ("0") and
+  Zero :: nat    (\<open>0\<close>) and
   Suc :: "nat => nat" and
   rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
 where
@@ -46,7 +46,7 @@
 qed
 
 
-definition add :: "nat => nat => nat"    (infixl "+" 60)
+definition add :: "nat => nat => nat"    (infixl \<open>+\<close> 60)
   where "m + n = rec(m, n, \<lambda>x y. Suc(y))"
 
 lemma add_0 [simp]: "0 + n = n"
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/FOL/ex/Prolog.thy
--- a/src/FOL/ex/Prolog.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/FOL/ex/Prolog.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -14,7 +14,7 @@
 
 axiomatization
   Nil     :: "'a list" and
-  Cons    :: "['a, 'a list]=> 'a list"    (infixr ":" 60) and
+  Cons    :: "['a, 'a list]=> 'a list"    (infixr \<open>:\<close> 60) and
   app     :: "['a list, 'a list, 'a list] => o" and
   rev     :: "['a list, 'a list] => o"
 where
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Arith.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -43,15 +43,15 @@
   "raw_mult(succ(m), n) = raw_add (n, raw_mult(m, n))"
 
 definition
-  add :: "[i,i]=>i"                    (infixl "#+" 65)  where
+  add :: "[i,i]=>i"                    (infixl \<open>#+\<close> 65)  where
     "m #+ n == raw_add (natify(m), natify(n))"
 
 definition
-  diff :: "[i,i]=>i"                    (infixl "#-" 65)  where
+  diff :: "[i,i]=>i"                    (infixl \<open>#-\<close> 65)  where
     "m #- n == raw_diff (natify(m), natify(n))"
 
 definition
-  mult :: "[i,i]=>i"                    (infixl "#*" 70)  where
+  mult :: "[i,i]=>i"                    (infixl \<open>#*\<close> 70)  where
     "m #* n == raw_mult (natify(m), natify(n))"
 
 definition
@@ -65,11 +65,11 @@
        transrec(m, %j f. if j<n | n=0 then j else f`(j#-n))"
 
 definition
-  div  :: "[i,i]=>i"                    (infixl "div" 70)  where
+  div  :: "[i,i]=>i"                    (infixl \<open>div\<close> 70)  where
     "m div n == raw_div (natify(m), natify(n))"
 
 definition
-  mod  :: "[i,i]=>i"                    (infixl "mod" 70)  where
+  mod  :: "[i,i]=>i"                    (infixl \<open>mod\<close> 70)  where
     "m mod n == raw_mod (natify(m), natify(n))"
 
 declare rec_type [simp]
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Bin.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -23,7 +23,7 @@
 datatype
   "bin" = Pls
         | Min
-        | Bit ("w \<in> bin", "b \<in> bool")     (infixl "BIT" 90)
+        | Bit ("w \<in> bin", "b \<in> bool")     (infixl \<open>BIT\<close> 90)
 
 consts
   integ_of  :: "i=>i"
@@ -101,11 +101,11 @@
                                  NCons(bin_mult(v,w),0))"
 
 syntax
-  "_Int0" :: i  ("#()0")
-  "_Int1" :: i  ("#()1")
-  "_Int2" :: i  ("#()2")
-  "_Neg_Int1" :: i  ("#-()1")
-  "_Neg_Int2" :: i  ("#-()2")
+  "_Int0" :: i  (\<open>#()0\<close>)
+  "_Int1" :: i  (\<open>#()1\<close>)
+  "_Int2" :: i  (\<open>#()2\<close>)
+  "_Neg_Int1" :: i  (\<open>#-()1\<close>)
+  "_Neg_Int2" :: i  (\<open>#-()2\<close>)
 translations
   "#0" \<rightleftharpoons> "CONST integ_of(CONST Pls)"
   "#1" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1)"
@@ -114,8 +114,8 @@
   "#-2" \<rightleftharpoons> "CONST integ_of(CONST Min BIT 0)"
 
 syntax
-  "_Int" :: "num_token => i"  ("#_" 1000)
-  "_Neg_Int" :: "num_token => i"  ("#-_" 1000)
+  "_Int" :: "num_token => i"  (\<open>#_\<close> 1000)
+  "_Neg_Int" :: "num_token => i"  (\<open>#-_\<close> 1000)
 
 ML_file "Tools/numeral_syntax.ML"
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Bool.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -8,11 +8,11 @@
 theory Bool imports pair begin
 
 abbreviation
-  one  ("1") where
+  one  (\<open>1\<close>) where
   "1 == succ(0)"
 
 abbreviation
-  two  ("2") where
+  two  (\<open>2\<close>) where
   "2 == succ(1)"
 
 text\<open>2 is equal to bool, but is used as a number rather than a type.\<close>
@@ -24,15 +24,15 @@
 definition "not(b) == cond(b,0,1)"
 
 definition
-  "and"       :: "[i,i]=>i"      (infixl "and" 70)  where
+  "and"       :: "[i,i]=>i"      (infixl \<open>and\<close> 70)  where
     "a and b == cond(a,b,0)"
 
 definition
-  or          :: "[i,i]=>i"      (infixl "or" 65)  where
+  or          :: "[i,i]=>i"      (infixl \<open>or\<close> 65)  where
     "a or b == cond(a,1,b)"
 
 definition
-  xor         :: "[i,i]=>i"      (infixl "xor" 65) where
+  xor         :: "[i,i]=>i"      (infixl \<open>xor\<close> 65) where
     "a xor b == cond(a,not(b),b)"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Cardinal.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -9,23 +9,23 @@
 
 definition
   (*least ordinal operator*)
-   Least    :: "(i=>o) => i"    (binder "\<mu> " 10)  where
+   Least    :: "(i=>o) => i"    (binder \<open>\<mu> \<close> 10)  where
      "Least(P) == THE i. Ord(i) & P(i) & (\<forall>j. j<i \<longrightarrow> ~P(j))"
 
 definition
-  eqpoll   :: "[i,i] => o"     (infixl "\<approx>" 50)  where
+  eqpoll   :: "[i,i] => o"     (infixl \<open>\<approx>\<close> 50)  where
     "A \<approx> B == \<exists>f. f \<in> bij(A,B)"
 
 definition
-  lepoll   :: "[i,i] => o"     (infixl "\<lesssim>" 50)  where
+  lepoll   :: "[i,i] => o"     (infixl \<open>\<lesssim>\<close> 50)  where
     "A \<lesssim> B == \<exists>f. f \<in> inj(A,B)"
 
 definition
-  lesspoll :: "[i,i] => o"     (infixl "\<prec>" 50)  where
+  lesspoll :: "[i,i] => o"     (infixl \<open>\<prec>\<close> 50)  where
     "A \<prec> B == A \<lesssim> B & ~(A \<approx> B)"
 
 definition
-  cardinal :: "i=>i"           ("|_|")  where
+  cardinal :: "i=>i"           (\<open>|_|\<close>)  where
     "|A| == (\<mu> i. i \<approx> A)"
 
 definition
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/CardinalArith.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -12,11 +12,11 @@
     "InfCard(i) == Card(i) & nat \<le> i"
 
 definition
-  cmult         :: "[i,i]=>i"       (infixl "\<otimes>" 70)  where
+  cmult         :: "[i,i]=>i"       (infixl \<open>\<otimes>\<close> 70)  where
     "i \<otimes> j == |i*j|"
 
 definition
-  cadd          :: "[i,i]=>i"       (infixl "\<oplus>" 65)  where
+  cadd          :: "[i,i]=>i"       (infixl \<open>\<oplus>\<close> 65)  where
     "i \<oplus> j == |i+j|"
 
 definition
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Constructible/L_axioms.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -130,7 +130,7 @@
 text\<open>We must use the meta-existential quantifier; otherwise the reflection
       terms become enormous!\<close>
 definition
-  L_Reflects :: "[i=>o,[i,i]=>o] => prop"  ("(3REFLECTS/ [_,/ _])") where
+  L_Reflects :: "[i=>o,[i,i]=>o] => prop"  (\<open>(3REFLECTS/ [_,/ _])\<close>) where
     "REFLECTS[P,Q] == (\<Or>Cl. Closed_Unbounded(Cl) &
                            (\<forall>a. Cl(a) \<longrightarrow> (\<forall>x \<in> Lset(a). P(x) \<longleftrightarrow> Q(a,x))))"
 
@@ -268,25 +268,25 @@
 subsubsection\<open>Some numbers to help write de Bruijn indices\<close>
 
 abbreviation
-  digit3 :: i   ("3") where "3 == succ(2)"
+  digit3 :: i   (\<open>3\<close>) where "3 == succ(2)"
 
 abbreviation
-  digit4 :: i   ("4") where "4 == succ(3)"
+  digit4 :: i   (\<open>4\<close>) where "4 == succ(3)"
 
 abbreviation
-  digit5 :: i   ("5") where "5 == succ(4)"
+  digit5 :: i   (\<open>5\<close>) where "5 == succ(4)"
 
 abbreviation
-  digit6 :: i   ("6") where "6 == succ(5)"
+  digit6 :: i   (\<open>6\<close>) where "6 == succ(5)"
 
 abbreviation
-  digit7 :: i   ("7") where "7 == succ(6)"
+  digit7 :: i   (\<open>7\<close>) where "7 == succ(6)"
 
 abbreviation
-  digit8 :: i   ("8") where "8 == succ(7)"
+  digit8 :: i   (\<open>8\<close>) where "8 == succ(7)"
 
 abbreviation
-  digit9 :: i   ("9") where "9 == succ(8)"
+  digit9 :: i   (\<open>9\<close>) where "9 == succ(8)"
 
 
 subsubsection\<open>The Empty Set, Internalized\<close>
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Constructible/MetaExists.thy
--- a/src/ZF/Constructible/MetaExists.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Constructible/MetaExists.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -10,7 +10,7 @@
 Yields a proposition rather than a FOL formula.\<close>
 
 definition
-  ex :: "(('a::{}) \<Rightarrow> prop) \<Rightarrow> prop"  (binder "\<Or>" 0) where
+  ex :: "(('a::{}) \<Rightarrow> prop) \<Rightarrow> prop"  (binder \<open>\<Or>\<close> 0) where
   "ex(P) == (\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q)"
 
 lemma meta_exI: "PROP P(x) ==> (\<Or>x. PROP P(x))"
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Constructible/Normal.thy
--- a/src/ZF/Constructible/Normal.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Constructible/Normal.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -456,7 +456,7 @@
 numbers.\<close>
 
 definition
-  Aleph :: "i => i"  ("\<aleph>_" [90] 90) where
+  Aleph :: "i => i"  (\<open>\<aleph>_\<close> [90] 90) where
     "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
 
 lemma Card_Aleph [simp, intro]:
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/EquivClass.thy
--- a/src/ZF/EquivClass.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/EquivClass.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -8,7 +8,7 @@
 theory EquivClass imports Trancl Perm begin
 
 definition
-  quotient   :: "[i,i]=>i"    (infixl "'/'/" 90)  (*set of equiv classes*)  where
+  quotient   :: "[i,i]=>i"    (infixl \<open>'/'/\<close> 90)  (*set of equiv classes*)  where
       "A//r == {r``{x} . x \<in> A}"
 
 definition
@@ -21,11 +21,11 @@
            <y1,z1>:r1 \<longrightarrow> <y2,z2>:r2 \<longrightarrow> b(y1,y2) = b(z1,z2)"
 
 abbreviation
-  RESPECTS ::"[i=>i, i] => o"  (infixr "respects" 80) where
+  RESPECTS ::"[i=>i, i] => o"  (infixr \<open>respects\<close> 80) where
   "f respects r == congruent(r,f)"
 
 abbreviation
-  RESPECTS2 ::"[i=>i=>i, i] => o"  (infixr "respects2 " 80) where
+  RESPECTS2 ::"[i=>i=>i, i] => o"  (infixr \<open>respects2 \<close> 80) where
   "f respects2 r == congruent2(r,r,f)"
     \<comment> \<open>Abbreviation for the common case where the relations are identical\<close>
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Finite.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -19,7 +19,7 @@
 
 consts
   Fin       :: "i=>i"
-  FiniteFun :: "[i,i]=>i"         ("(_ -||>/ _)" [61, 60] 60)
+  FiniteFun :: "[i,i]=>i"         (\<open>(_ -||>/ _)\<close> [61, 60] 60)
 
 inductive
   domains   "Fin(A)" \<subseteq> "Pow(A)"
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/IMP/Com.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -23,7 +23,7 @@
 consts evala :: i
 
 abbreviation
-  evala_syntax :: "[i, i] => o"    (infixl "-a->" 50)
+  evala_syntax :: "[i, i] => o"    (infixl \<open>-a->\<close> 50)
   where "p -a-> n == <p,n> \<in> evala"
 
 inductive
@@ -46,14 +46,14 @@
        | false
        | ROp  ("f \<in> (nat \<times> nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp")
        | noti ("b \<in> bexp")
-       | andi ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl "andi" 60)
-       | ori  ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl "ori" 60)
+       | andi ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl \<open>andi\<close> 60)
+       | ori  ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl \<open>ori\<close> 60)
 
 
 consts evalb :: i
 
 abbreviation
-  evalb_syntax :: "[i,i] => o"    (infixl "-b->" 50)
+  evalb_syntax :: "[i,i] => o"    (infixl \<open>-b->\<close> 50)
   where "p -b-> b == <p,b> \<in> evalb"
 
 inductive
@@ -77,17 +77,17 @@
 
 consts com :: i
 datatype com =
-    skip                                  ("\<SKIP>" [])
-  | assignment ("x \<in> loc", "a \<in> aexp")       (infixl "\<ASSN>" 60)
-  | semicolon ("c0 \<in> com", "c1 \<in> com")       ("_\<SEQ> _"  [60, 60] 10)
-  | while ("b \<in> bexp", "c \<in> com")            ("\<WHILE> _ \<DO> _"  60)
-  | "if" ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com")    ("\<IF> _ \<THEN> _ \<ELSE> _" 60)
+    skip                                  (\<open>\<SKIP>\<close> [])
+  | assignment ("x \<in> loc", "a \<in> aexp")       (infixl \<open>\<ASSN>\<close> 60)
+  | semicolon ("c0 \<in> com", "c1 \<in> com")       (\<open>_\<SEQ> _\<close>  [60, 60] 10)
+  | while ("b \<in> bexp", "c \<in> com")            (\<open>\<WHILE> _ \<DO> _\<close>  60)
+  | "if" ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com")    (\<open>\<IF> _ \<THEN> _ \<ELSE> _\<close> 60)
 
 
 consts evalc :: i
 
 abbreviation
-  evalc_syntax :: "[i, i] => o"    (infixl "-c->" 50)
+  evalc_syntax :: "[i, i] => o"    (infixl \<open>-c->\<close> 50)
   where "p -c-> s == <p,s> \<in> evalc"
 
 inductive
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/IMP/Denotation.thy
--- a/src/ZF/IMP/Denotation.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/IMP/Denotation.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -14,7 +14,7 @@
   C     :: "i => i"
 
 definition
-  Gamma :: "[i,i,i] => i"  ("\<Gamma>") where
+  Gamma :: "[i,i,i] => i"  (\<open>\<Gamma>\<close>) where
   "\<Gamma>(b,cden) ==
     (\<lambda>phi. {io \<in> (phi O cden). B(b,fst(io))=1} \<union>
            {io \<in> id(loc->nat). B(b,fst(io))=0})"
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Induct/Comb.thy
--- a/src/ZF/Induct/Comb.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Induct/Comb.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -24,7 +24,7 @@
 datatype comb =
   K
 | S
-| app ("p \<in> comb", "q \<in> comb")  (infixl "\<bullet>" 90)
+| app ("p \<in> comb", "q \<in> comb")  (infixl \<open>\<bullet>\<close> 90)
 
 text \<open>
   Inductive definition of contractions, \<open>\<rightarrow>\<^sup>1\<close> and
@@ -32,10 +32,10 @@
 \<close>
 
 consts contract  :: i
-abbreviation contract_syntax :: "[i,i] \<Rightarrow> o"  (infixl "\<rightarrow>\<^sup>1" 50)
+abbreviation contract_syntax :: "[i,i] \<Rightarrow> o"  (infixl \<open>\<rightarrow>\<^sup>1\<close> 50)
   where "p \<rightarrow>\<^sup>1 q \<equiv> <p,q> \<in> contract"
 
-abbreviation contract_multi :: "[i,i] \<Rightarrow> o"  (infixl "\<rightarrow>" 50)
+abbreviation contract_multi :: "[i,i] \<Rightarrow> o"  (infixl \<open>\<rightarrow>\<close> 50)
   where "p \<rightarrow> q \<equiv> <p,q> \<in> contract^*"
 
 inductive
@@ -54,10 +54,10 @@
 
 consts parcontract :: i
 
-abbreviation parcontract_syntax :: "[i,i] => o"  (infixl "\<Rrightarrow>\<^sup>1" 50)
+abbreviation parcontract_syntax :: "[i,i] => o"  (infixl \<open>\<Rrightarrow>\<^sup>1\<close> 50)
   where "p \<Rrightarrow>\<^sup>1 q == <p,q> \<in> parcontract"
 
-abbreviation parcontract_multi :: "[i,i] => o"  (infixl "\<Rrightarrow>" 50)
+abbreviation parcontract_multi :: "[i,i] => o"  (infixl \<open>\<Rrightarrow>\<close> 50)
   where "p \<Rrightarrow> q == <p,q> \<in> parcontract^+"
 
 inductive
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Induct/FoldSet.thy
--- a/src/ZF/Induct/FoldSet.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Induct/FoldSet.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -19,7 +19,7 @@
   type_intros Fin.intros
   
 definition
-  fold :: "[i, [i,i]=>i, i, i] => i"  ("fold[_]'(_,_,_')")  where
+  fold :: "[i, [i,i]=>i, i, i] => i"  (\<open>fold[_]'(_,_,_')\<close>)  where
    "fold[B](f,e, A) == THE x. <A, x>\<in>fold_set(A, B, f,e)"
 
 definition
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Induct/Multiset.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -33,7 +33,7 @@
   "mset_of(M) == domain(M)"
 
 definition
-  munion    :: "[i, i] => i" (infixl "+#" 65)  where
+  munion    :: "[i, i] => i" (infixl \<open>+#\<close> 65)  where
   "M +# N == \<lambda>x \<in> mset_of(M) \<union> mset_of(N).
      if x \<in> mset_of(M) \<inter> mset_of(N) then  (M`x) #+ (N`x)
      else (if x \<in> mset_of(M) then M`x else N`x)"
@@ -47,13 +47,13 @@
        else 0"
 
 definition
-  mdiff  :: "[i, i] => i" (infixl "-#" 65)  where
+  mdiff  :: "[i, i] => i" (infixl \<open>-#\<close> 65)  where
   "M -# N ==  normalize(\<lambda>x \<in> mset_of(M).
                         if x \<in> mset_of(N) then M`x #- N`x else M`x)"
 
 definition
   (* set of elements of a multiset *)
-  msingle :: "i => i"    ("{#_#}")  where
+  msingle :: "i => i"    (\<open>{#_#}\<close>)  where
   "{#a#} == {<a, 1>}"
 
 definition
@@ -70,11 +70,11 @@
   "msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))"
 
 abbreviation
-  melem :: "[i,i] => o"    ("(_/ :# _)" [50, 51] 50)  where
+  melem :: "[i,i] => o"    (\<open>(_/ :# _)\<close> [50, 51] 50)  where
   "a :# M == a \<in> mset_of(M)"
 
 syntax
-  "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
+  "_MColl" :: "[pttrn, i, o] => i" (\<open>(1{# _ \<in> _./ _#})\<close>)
 translations
   "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
 
@@ -100,11 +100,11 @@
   "omultiset(M) == \<exists>i. Ord(i) & M \<in> Mult(field(Memrel(i)))"
 
 definition
-  mless :: "[i, i] => o" (infixl "<#" 50)  where
+  mless :: "[i, i] => o" (infixl \<open><#\<close> 50)  where
   "M <# N ==  \<exists>i. Ord(i) & <M, N> \<in> multirel(field(Memrel(i)), Memrel(i))"
 
 definition
-  mle  :: "[i, i] => o"  (infixl "<#=" 50)  where
+  mle  :: "[i, i] => o"  (infixl \<open><#=\<close> 50)  where
   "M <#= N == (omultiset(M) & M = N) | M <# N"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Induct/PropLog.thy
--- a/src/ZF/Induct/PropLog.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Induct/PropLog.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -26,8 +26,8 @@
 
 datatype propn =
     Fls
-  | Var ("n \<in> nat")    ("#_" [100] 100)
-  | Imp ("p \<in> propn", "q \<in> propn")    (infixr "=>" 90)
+  | Var ("n \<in> nat")    (\<open>#_\<close> [100] 100)
+  | Imp ("p \<in> propn", "q \<in> propn")    (infixr \<open>=>\<close> 90)
 
 
 subsection \<open>The proof system\<close>
@@ -35,7 +35,7 @@
 consts thms     :: "i => i"
 
 abbreviation
-  thms_syntax :: "[i,i] => o"    (infixl "|-" 50)
+  thms_syntax :: "[i,i] => o"    (infixl \<open>|-\<close> 50)
   where "H |- p == p \<in> thms(H)"
 
 inductive
@@ -86,7 +86,7 @@
 \<close>
 
 definition
-  logcon :: "[i,i] => o"    (infixl "|=" 50)  where
+  logcon :: "[i,i] => o"    (infixl \<open>|=\<close> 50)  where
   "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) \<longrightarrow> is_true(p,t)"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Int.thy
--- a/src/ZF/Int.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Int.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -17,7 +17,7 @@
     "int == (nat*nat)//intrel"
 
 definition
-  int_of :: "i=>i" \<comment> \<open>coercion from nat to int\<close>    ("$# _" [80] 80)  where
+  int_of :: "i=>i" \<comment> \<open>coercion from nat to int\<close>    (\<open>$# _\<close> [80] 80)  where
     "$# m == intrel `` {<natify(m), 0>}"
 
 definition
@@ -29,7 +29,7 @@
     "raw_zminus(z) == \<Union><x,y>\<in>z. intrel``{<y,x>}"
 
 definition
-  zminus :: "i=>i"                                 ("$- _" [80] 80)  where
+  zminus :: "i=>i"                                 (\<open>$- _\<close> [80] 80)  where
     "$- z == raw_zminus (intify(z))"
 
 definition
@@ -65,7 +65,7 @@
                    intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
 
 definition
-  zmult       ::      "[i,i]=>i"      (infixl "$*" 70)  where
+  zmult       ::      "[i,i]=>i"      (infixl \<open>$*\<close> 70)  where
      "z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
 
 definition
@@ -75,19 +75,19 @@
                            in intrel``{<x1#+x2, y1#+y2>}"
 
 definition
-  zadd        ::      "[i,i]=>i"      (infixl "$+" 65)  where
+  zadd        ::      "[i,i]=>i"      (infixl \<open>$+\<close> 65)  where
      "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
 
 definition
-  zdiff        ::      "[i,i]=>i"      (infixl "$-" 65)  where
+  zdiff        ::      "[i,i]=>i"      (infixl \<open>$-\<close> 65)  where
      "z1 $- z2 == z1 $+ zminus(z2)"
 
 definition
-  zless        ::      "[i,i]=>o"      (infixl "$<" 50)  where
+  zless        ::      "[i,i]=>o"      (infixl \<open>$<\<close> 50)  where
      "z1 $< z2 == znegative(z1 $- z2)"
 
 definition
-  zle          ::      "[i,i]=>o"      (infixl "$\<le>" 50)  where
+  zle          ::      "[i,i]=>o"      (infixl \<open>$\<le>\<close> 50)  where
      "z1 $\<le> z2 == z1 $< z2 | intify(z1)=intify(z2)"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/IntDiv.thy
--- a/src/ZF/IntDiv.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/IntDiv.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -88,11 +88,11 @@
                   else         negateSnd (posDivAlg (<$-a,$-b>))"
 
 definition
-  zdiv  :: "[i,i]=>i"                    (infixl "zdiv" 70)  where
+  zdiv  :: "[i,i]=>i"                    (infixl \<open>zdiv\<close> 70)  where
     "a zdiv b == fst (divAlg (<intify(a), intify(b)>))"
 
 definition
-  zmod  :: "[i,i]=>i"                    (infixl "zmod" 70)  where
+  zmod  :: "[i,i]=>i"                    (infixl \<open>zmod\<close> 70)  where
     "a zmod b == snd (divAlg (<intify(a), intify(b)>))"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/List.thy
--- a/src/ZF/List.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/List.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -15,8 +15,8 @@
 
 
 syntax
- "_Nil" :: i  ("[]")
- "_List" :: "is => i"  ("[(_)]")
+ "_Nil" :: i  (\<open>[]\<close>)
+ "_List" :: "is => i"  (\<open>[(_)]\<close>)
 
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
@@ -45,7 +45,7 @@
 consts
   map         :: "[i=>i, i] => i"
   set_of_list :: "i=>i"
-  app         :: "[i,i]=>i"                        (infixr "@" 60)
+  app         :: "[i,i]=>i"                        (infixr \<open>@\<close> 60)
 
 (*map is a binding operator -- it applies to meta-level functions, not
 object-level functions.  This simplifies the final form of term_rec_conv,
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/OrdQuant.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -23,9 +23,9 @@
     "OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
 
 syntax
-  "_oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
-  "_oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
-  "_OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
+  "_oall"     :: "[idt, i, o] => o"        (\<open>(3\<forall>_<_./ _)\<close> 10)
+  "_oex"      :: "[idt, i, o] => o"        (\<open>(3\<exists>_<_./ _)\<close> 10)
+  "_OUNION"   :: "[idt, i, i] => i"        (\<open>(3\<Union>_<_./ _)\<close> 10)
 translations
   "\<forall>x<a. P" \<rightleftharpoons> "CONST oall(a, \<lambda>x. P)"
   "\<exists>x<a. P" \<rightleftharpoons> "CONST oex(a, \<lambda>x. P)"
@@ -192,8 +192,8 @@
     "rex(M, P) == \<exists>x. M(x) & P(x)"
 
 syntax
-  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
-  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
+  "_rall"     :: "[pttrn, i=>o, o] => o"        (\<open>(3\<forall>_[_]./ _)\<close> 10)
+  "_rex"      :: "[pttrn, i=>o, o] => o"        (\<open>(3\<exists>_[_]./ _)\<close> 10)
 translations
   "\<forall>x[M]. P" \<rightleftharpoons> "CONST rall(M, \<lambda>x. P)"
   "\<exists>x[M]. P" \<rightleftharpoons> "CONST rex(M, \<lambda>x. P)"
@@ -323,7 +323,7 @@
 subsubsection\<open>Sets as Classes\<close>
 
 definition
-  setclass :: "[i,i] => o"       ("##_" [40] 40)  where
+  setclass :: "[i,i] => o"       (\<open>##_\<close> [40] 40)  where
    "setclass(A) == %x. x \<in> A"
 
 lemma setclass_iff [simp]: "setclass(A,x) <-> x \<in> A"
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Order.thy
--- a/src/ZF/Order.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Order.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -49,7 +49,7 @@
               {f \<in> A->B. \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longrightarrow> <f`x,f`y>:s}"
 
 definition
-  ord_iso  :: "[i,i,i,i]=>i"  ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)  (*Order isomorphisms*)  where
+  ord_iso  :: "[i,i,i,i]=>i"  (\<open>(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)\<close> 51)  (*Order isomorphisms*)  where
    "\<langle>A,r\<rangle> \<cong> \<langle>B,s\<rangle> ==
               {f \<in> bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longleftrightarrow> <f`x,f`y>:s}"
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/OrderType.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -31,7 +31,7 @@
 
 definition
   (*ordinal multiplication*)
-  omult      :: "[i,i]=>i"           (infixl "**" 70)  where
+  omult      :: "[i,i]=>i"           (infixl \<open>**\<close> 70)  where
    "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
 
 definition
@@ -40,12 +40,12 @@
     "raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
 
 definition
-  oadd      :: "[i,i]=>i"           (infixl "++" 65)  where
+  oadd      :: "[i,i]=>i"           (infixl \<open>++\<close> 65)  where
     "i ++ j == raw_oadd(ordify(i),ordify(j))"
 
 definition
   (*ordinal subtraction*)
-  odiff      :: "[i,i]=>i"           (infixl "--" 65)  where
+  odiff      :: "[i,i]=>i"           (infixl \<open>--\<close> 65)  where
     "i -- j == ordertype(i-j, Memrel(i))"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Ordinal.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -20,7 +20,7 @@
     "Ord(i)      == Transset(i) & (\<forall>x\<in>i. Transset(x))"
 
 definition
-  lt        :: "[i,i] => o"  (infixl "<" 50)   (*less-than on ordinals*)  where
+  lt        :: "[i,i] => o"  (infixl \<open><\<close> 50)   (*less-than on ordinals*)  where
     "i<j         == i\<in>j & Ord(j)"
 
 definition
@@ -28,7 +28,7 @@
     "Limit(i)    == Ord(i) & 0<i & (\<forall>y. y<i \<longrightarrow> succ(y)<i)"
 
 abbreviation
-  le  (infixl "\<le>" 50) where
+  le  (infixl \<open>\<le>\<close> 50) where
   "x \<le> y == x < succ(y)"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Perm.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -14,7 +14,7 @@
 
 definition
   (*composition of relations and functions; NOT Suppes's relative product*)
-  comp     :: "[i,i]=>i"      (infixr "O" 60)  where
+  comp     :: "[i,i]=>i"      (infixr \<open>O\<close> 60)  where
     "r O s == {xz \<in> domain(s)*range(r) .
                \<exists>x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/QPair.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -21,7 +21,7 @@
 \<close>
 
 definition
-  QPair     :: "[i, i] => i"                      ("<(_;/ _)>")  where
+  QPair     :: "[i, i] => i"                      (\<open><(_;/ _)>\<close>)  where
     "<a;b> == a+b"
 
 definition
@@ -45,16 +45,16 @@
     "QSigma(A,B)  ==  \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
 
 syntax
-  "_QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _ \<in> _./ _)" 10)
+  "_QSUM"   :: "[idt, i, i] => i"               (\<open>(3QSUM _ \<in> _./ _)\<close> 10)
 translations
   "QSUM x \<in> A. B"  => "CONST QSigma(A, %x. B)"
 
 abbreviation
-  qprod  (infixr "<*>" 80) where
+  qprod  (infixr \<open><*>\<close> 80) where
   "A <*> B == QSigma(A, %_. B)"
 
 definition
-  qsum    :: "[i,i]=>i"                         (infixr "<+>" 65)  where
+  qsum    :: "[i,i]=>i"                         (infixr \<open><+>\<close> 65)  where
     "A <+> B      == ({0} <*> A) \<union> ({1} <*> B)"
 
 definition
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Resid/Confluence.thy
--- a/src/ZF/Resid/Confluence.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Resid/Confluence.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -68,11 +68,11 @@
   Sconv         :: "i"
 
 abbreviation
-  Sconv1_rel (infixl "<-1->" 50) where
+  Sconv1_rel (infixl \<open><-1->\<close> 50) where
   "a<-1->b == <a,b> \<in> Sconv1"
 
 abbreviation
-  Sconv_rel (infixl "<-\<longrightarrow>" 50) where
+  Sconv_rel (infixl \<open><-\<longrightarrow>\<close> 50) where
   "a<-\<longrightarrow>b == <a,b> \<in> Sconv"
   
 inductive
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Resid/Redex.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -18,11 +18,11 @@
   Sreg  :: "i"
 
 abbreviation
-  Ssub_rel  (infixl "\<Longleftarrow>" 70) where
+  Ssub_rel  (infixl \<open>\<Longleftarrow>\<close> 70) where
   "a \<Longleftarrow> b == <a,b> \<in> Ssub"
 
 abbreviation
-  Scomp_rel  (infixl "\<sim>" 70) where
+  Scomp_rel  (infixl \<open>\<sim>\<close> 70) where
   "a \<sim> b == <a,b> \<in> Scomp"
 
 abbreviation
@@ -43,7 +43,7 @@
                      %c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
 
 definition
-  union  (infixl "\<squnion>" 70) where
+  union  (infixl \<open>\<squnion>\<close> 70) where
   "u \<squnion> v == union_aux(u)`v"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Resid/Reduction.thy
--- a/src/ZF/Resid/Reduction.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Resid/Reduction.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -74,19 +74,19 @@
   Spar_red  :: "i"
 
 abbreviation
-  Sred1_rel (infixl "-1->" 50) where
+  Sred1_rel (infixl \<open>-1->\<close> 50) where
   "a -1-> b == <a,b> \<in> Sred1"
 
 abbreviation
-  Sred_rel (infixl "-\<longrightarrow>" 50) where
+  Sred_rel (infixl \<open>-\<longrightarrow>\<close> 50) where
   "a -\<longrightarrow> b == <a,b> \<in> Sred"
 
 abbreviation
-  Spar_red1_rel (infixl "=1=>" 50) where
+  Spar_red1_rel (infixl \<open>=1=>\<close> 50) where
   "a =1=> b == <a,b> \<in> Spar_red1"
 
 abbreviation
-  Spar_red_rel (infixl "===>" 50) where
+  Spar_red_rel (infixl \<open>===>\<close> 50) where
   "a ===> b == <a,b> \<in> Spar_red"
   
   
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Resid/Residuals.thy
--- a/src/ZF/Resid/Residuals.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Resid/Residuals.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -26,7 +26,7 @@
   type_intros    subst_type nat_typechecks redexes.intros bool_typechecks
 
 definition
-  res_func      :: "[i,i]=>i"     (infixl "|>" 70)  where
+  res_func      :: "[i,i]=>i"     (infixl \<open>|>\<close> 70)  where
   "u |> v == THE w. residuals(u,v,w)"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Resid/Substitution.thy
--- a/src/ZF/Resid/Substitution.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Resid/Substitution.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -42,7 +42,7 @@
     "subst_rec(u,r,k) == subst_aux(r)`u`k"
 
 abbreviation
-  subst :: "[i,i]=>i"  (infixl "'/" 70)  where
+  subst :: "[i,i]=>i"  (infixl \<open>'/\<close> 70)  where
   "u/v == subst_rec(u,v,0)"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Sum.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -9,7 +9,7 @@
 
 text\<open>And the "Part" primitive for simultaneous recursive type definitions\<close>
 
-definition sum :: "[i,i]=>i" (infixr "+" 65) where
+definition sum :: "[i,i]=>i" (infixr \<open>+\<close> 65) where
      "A+B == {0}*A \<union> {1}*B"
 
 definition Inl :: "i=>i" where
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Trancl.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -32,16 +32,16 @@
     "trans(r) == \<forall>x y z. <x,y>: r \<longrightarrow> <y,z>: r \<longrightarrow> <x,z>: r"
 
 definition
-  trans_on :: "[i,i]=>o"  ("trans[_]'(_')")  where
+  trans_on :: "[i,i]=>o"  (\<open>trans[_]'(_')\<close>)  where
     "trans[A](r) == \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A.
                           <x,y>: r \<longrightarrow> <y,z>: r \<longrightarrow> <x,z>: r"
 
 definition
-  rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)  where
+  rtrancl :: "i=>i"  (\<open>(_^*)\<close> [100] 100)  (*refl/transitive closure*)  where
     "r^* == lfp(field(r)*field(r), %s. id(field(r)) \<union> (r O s))"
 
 definition
-  trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)  where
+  trancl  :: "i=>i"  (\<open>(_^+)\<close> [100] 100)  (*transitive closure*)  where
     "r^+ == r O r^*"
 
 definition
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/UNITY/Comp.thy
--- a/src/ZF/UNITY/Comp.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/Comp.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -18,20 +18,20 @@
 theory Comp imports Union Increasing begin
 
 definition
-  component :: "[i,i]=>o"  (infixl "component" 65)  where
+  component :: "[i,i]=>o"  (infixl \<open>component\<close> 65)  where
   "F component H == (\<exists>G. F \<squnion> G = H)"
 
 definition
-  strict_component :: "[i,i]=>o" (infixl "strict'_component" 65)  where
+  strict_component :: "[i,i]=>o" (infixl \<open>strict'_component\<close> 65)  where
   "F strict_component H == F component H & F\<noteq>H"
 
 definition
   (* A stronger form of the component relation *)
-  component_of :: "[i,i]=>o"   (infixl "component'_of" 65)  where
+  component_of :: "[i,i]=>o"   (infixl \<open>component'_of\<close> 65)  where
   "F component_of H  == (\<exists>G. F ok G & F \<squnion> G = H)"
   
 definition
-  strict_component_of :: "[i,i]=>o" (infixl "strict'_component'_of" 65)  where
+  strict_component_of :: "[i,i]=>o" (infixl \<open>strict'_component'_of\<close> 65)  where
   "F strict_component_of H  == F component_of H  & F\<noteq>H"
 
 definition
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/Constrains.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -40,11 +40,11 @@
 
   
 definition
-  Constrains :: "[i,i] => i"  (infixl "Co" 60)  where
+  Constrains :: "[i,i] => i"  (infixl \<open>Co\<close> 60)  where
   "A Co B == {F:program. F:(reachable(F) \<inter> A) co B}"
 
 definition
-  op_Unless  :: "[i, i] => i"  (infixl "Unless" 60)  where
+  op_Unless  :: "[i, i] => i"  (infixl \<open>Unless\<close> 60)  where
   "A Unless B == (A-B) Co (A \<union> B)"
 
 definition
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/UNITY/Follows.thy
--- a/src/ZF/UNITY/Follows.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/Follows.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -34,12 +34,12 @@
   "m_Incr(f) == Increasing(Mult(nat), MultLe(nat, Le), f)"
 
 abbreviation
-  n_Fols :: "[i=>i, i=>i]=>i"   (infixl "n'_Fols" 65)  where
+  n_Fols :: "[i=>i, i=>i]=>i"   (infixl \<open>n'_Fols\<close> 65)  where
   "f n_Fols g == Follows(nat, Le, f, g)"
 
 abbreviation
   Follows' :: "[i=>i, i=>i, i, i] => i"
-        ("(_ /Fols _ /Wrt (_ /'/ _))" [60, 0, 0, 60] 60)  where
+        (\<open>(_ /Fols _ /Wrt (_ /'/ _))\<close> [60, 0, 0, 60] 60)  where
   "f Fols g Wrt r/A == Follows(A,r,f,g)"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/UNITY/GenPrefix.thy
--- a/src/ZF/UNITY/GenPrefix.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -49,11 +49,11 @@
 (* less or equal and greater or equal over prefixes *)
 
 abbreviation
-  pfixLe :: "[i, i] => o"  (infixl "pfixLe" 50)  where
+  pfixLe :: "[i, i] => o"  (infixl \<open>pfixLe\<close> 50)  where
   "xs pfixLe ys == <xs, ys>:gen_prefix(nat, Le)"
 
 abbreviation
-  pfixGe :: "[i, i] => o"  (infixl "pfixGe" 50)  where
+  pfixGe :: "[i, i] => o"  (infixl \<open>pfixGe\<close> 50)  where
   "xs pfixGe ys == <xs, ys>:gen_prefix(nat, Ge)"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/UNITY/Guar.thy
--- a/src/ZF/UNITY/Guar.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/Guar.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -57,7 +57,7 @@
     (SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow>(F \<in> X & G \<in> X) \<longleftrightarrow> (F \<squnion> G \<in> X)))"
 
 definition
-  guar :: "[i, i] => i" (infixl "guarantees" 55)  where
+  guar :: "[i, i] => i" (infixl \<open>guarantees\<close> 55)  where
               (*higher than membership, lower than Co*)
   "X guarantees Y == {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<squnion> G \<in> X \<longrightarrow> F \<squnion> G \<in> Y}"
   
@@ -77,13 +77,13 @@
   "welldef == {F \<in> program. Init(F) \<noteq> 0}"
   
 definition
-  refines :: "[i, i, i] => o" ("(3_ refines _ wrt _)" [10,10,10] 10)  where
+  refines :: "[i, i, i] => o" (\<open>(3_ refines _ wrt _)\<close> [10,10,10] 10)  where
   "G refines F wrt X ==
    \<forall>H \<in> program. (F ok H  & G ok H & F \<squnion> H \<in> welldef \<inter> X)
     \<longrightarrow> (G \<squnion> H \<in> welldef \<inter> X)"
 
 definition
-  iso_refines :: "[i,i, i] => o"  ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)  where
+  iso_refines :: "[i,i, i] => o"  (\<open>(3_ iso'_refines _ wrt _)\<close> [10,10,10] 10)  where
   "G iso_refines F wrt X ==  F \<in> welldef \<inter> X \<longrightarrow> G \<in> welldef \<inter> X"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/UNITY/Increasing.thy
--- a/src/ZF/UNITY/Increasing.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/Increasing.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -11,19 +11,19 @@
 theory Increasing imports Constrains Monotonicity begin
 
 definition
-  increasing :: "[i, i, i=>i] => i" ("increasing[_]'(_, _')")  where
+  increasing :: "[i, i, i=>i] => i" (\<open>increasing[_]'(_, _')\<close>)  where
   "increasing[A](r, f) ==
     {F \<in> program. (\<forall>k \<in> A. F \<in> stable({s \<in> state. <k, f(s)> \<in> r})) &
                 (\<forall>x \<in> state. f(x):A)}"
   
 definition
-  Increasing :: "[i, i, i=>i] => i" ("Increasing[_]'(_, _')")  where
+  Increasing :: "[i, i, i=>i] => i" (\<open>Increasing[_]'(_, _')\<close>)  where
   "Increasing[A](r, f) ==
     {F \<in> program. (\<forall>k \<in> A. F \<in> Stable({s \<in> state. <k, f(s)> \<in> r})) &
                 (\<forall>x \<in> state. f(x):A)}"
 
 abbreviation (input)
-  IncWrt ::  "[i=>i, i, i] => i" ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60)  where
+  IncWrt ::  "[i=>i, i, i] => i" (\<open>(_ IncreasingWrt _ '/ _)\<close> [60, 0, 60] 60)  where
   "f IncreasingWrt r/A == Increasing[A](r,f)"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/UNITY/SubstAx.thy
--- a/src/ZF/UNITY/SubstAx.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/SubstAx.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -13,11 +13,11 @@
 
 definition
   (* The definitions below are not `conventional', but yield simpler rules *)
-  Ensures :: "[i,i] => i"            (infixl "Ensures" 60)  where
+  Ensures :: "[i,i] => i"            (infixl \<open>Ensures\<close> 60)  where
   "A Ensures B == {F \<in> program. F \<in> (reachable(F) \<inter> A) ensures (reachable(F) \<inter> B) }"
 
 definition
-  LeadsTo :: "[i, i] => i"            (infixl "\<longmapsto>w" 60)  where
+  LeadsTo :: "[i, i] => i"            (infixl \<open>\<longmapsto>w\<close> 60)  where
   "A \<longmapsto>w B == {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> (reachable(F) \<inter> B)}"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/UNITY/UNITY.thy
--- a/src/ZF/UNITY/UNITY.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/UNITY.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -27,7 +27,7 @@
               cons(id(state), allowed \<inter> Pow(state*state))>"
 
 definition
-  SKIP :: i  ("\<bottom>") where
+  SKIP :: i  (\<open>\<bottom>\<close>) where
   "SKIP == mk_program(state, 0, Pow(state*state))"
 
   (* Coercion from anything to program *)
@@ -68,12 +68,12 @@
   initially :: "i=>i"  where
   "initially(A) == {F \<in> program. Init(F)\<subseteq>A}"
 
-definition "constrains" :: "[i, i] => i"  (infixl "co" 60)  where
+definition "constrains" :: "[i, i] => i"  (infixl \<open>co\<close> 60)  where
   "A co B == {F \<in> program. (\<forall>act \<in> Acts(F). act``A\<subseteq>B) & st_set(A)}"
     \<comment> \<open>the condition @{term "st_set(A)"} makes the definition slightly
          stronger than the HOL one\<close>
 
-definition unless :: "[i, i] => i"  (infixl "unless" 60)  where
+definition unless :: "[i, i] => i"  (infixl \<open>unless\<close> 60)  where
   "A unless B == (A - B) co (A \<union> B)"
 
 definition
@@ -90,7 +90,7 @@
 
   (* meta-function composition *)
 definition
-  metacomp :: "[i=>i, i=>i] => (i=>i)" (infixl "comp" 65)  where
+  metacomp :: "[i=>i, i=>i] => (i=>i)" (infixl \<open>comp\<close> 65)  where
   "f comp g == %x. f(g(x))"
 
 definition
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/UNITY/Union.thy
--- a/src/ZF/UNITY/Union.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/Union.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -15,7 +15,7 @@
 
 definition
   (*FIXME: conjoin Init(F) \<inter> Init(G) \<noteq> 0 *)
-  ok :: "[i, i] => o"     (infixl "ok" 65)  where
+  ok :: "[i, i] => o"     (infixl \<open>ok\<close> 65)  where
     "F ok G == Acts(F) \<subseteq> AllowedActs(G) &
                Acts(G) \<subseteq> AllowedActs(F)"
 
@@ -31,7 +31,7 @@
                  \<Inter>i \<in> I. AllowedActs(F(i)))"
 
 definition
-  Join :: "[i, i] => i"  (infixl "\<squnion>" 65)  where
+  Join :: "[i, i] => i"  (infixl \<open>\<squnion>\<close> 65)  where
   "F \<squnion> G == mk_program (Init(F) \<inter> Init(G), Acts(F) \<union> Acts(G),
                                 AllowedActs(F) \<inter> AllowedActs(G))"
 definition
@@ -41,8 +41,8 @@
       SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) \<longrightarrow> G \<in> X)"
 
 syntax
-  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion>_./ _)" 10)
-  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion>_ \<in> _./ _)" 10)
+  "_JOIN1"  :: "[pttrns, i] => i"     (\<open>(3\<Squnion>_./ _)\<close> 10)
+  "_JOIN"   :: "[pttrn, i, i] => i"   (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10)
 
 translations
   "\<Squnion>x \<in> A. B"   == "CONST JOIN(A, (\<lambda>x. B))"
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/UNITY/WFair.thy
--- a/src/ZF/UNITY/WFair.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/WFair.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -21,7 +21,7 @@
                                act``A \<subseteq> state-A) & st_set(A)}"
 
 definition
-  ensures :: "[i,i] => i"       (infixl "ensures" 60)  where
+  ensures :: "[i,i] => i"       (infixl \<open>ensures\<close> 60)  where
   "A ensures B == ((A-B) co (A \<union> B)) \<inter> transient(A-B)"
 
 consts
@@ -43,7 +43,7 @@
 
 definition
   (* The Visible version of the LEADS-TO relation*)
-  leadsTo :: "[i, i] => i"       (infixl "\<longmapsto>" 60)  where
+  leadsTo :: "[i, i] => i"       (infixl \<open>\<longmapsto>\<close> 60)  where
   "A \<longmapsto> B == {F \<in> program. <A,B>:leads(state, F)}"
 
 definition
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/WF.thy
--- a/src/ZF/WF.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/WF.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -24,7 +24,7 @@
     "wf(r) == \<forall>Z. Z=0 | (\<exists>x\<in>Z. \<forall>y. <y,x>:r \<longrightarrow> ~ y \<in> Z)"
 
 definition
-  wf_on        :: "[i,i]=>o"                      ("wf[_]'(_')")  where
+  wf_on        :: "[i,i]=>o"                      (\<open>wf[_]'(_')\<close>)  where
     (*r is well-founded on A*)
     "wf_on(A,r) == wf(r \<inter> A*A)"
 
@@ -46,7 +46,7 @@
     "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
 
 definition
-  wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"       ("wfrec[_]'(_,_,_')")  where
+  wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"       (\<open>wfrec[_]'(_,_,_')\<close>)  where
     "wfrec[A](r,a,H) == wfrec(r \<inter> A*A, a, H)"
 
 
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/ZF.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -7,14 +7,14 @@
 
 subsection\<open>Iteration of the function @{term F}\<close>
 
-consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)
+consts  iterates :: "[i=>i,i,i] => i"   (\<open>(_^_ '(_'))\<close> [60,1000,1000] 60)
 
 primrec
     "F^0 (x) = x"
     "F^(succ(n)) (x) = F(F^n (x))"
 
 definition
-  iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) where
+  iterates_omega :: "[i=>i,i] => i" (\<open>(_^\<omega> '(_'))\<close> [60,1000] 60) where
     "F^\<omega> (x) == \<Union>n\<in>nat. F^n (x)"
 
 lemma iterates_triv:
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/ZF_Base.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -16,14 +16,14 @@
 typedecl i
 instance i :: "term" ..
 
-axiomatization mem :: "[i, i] \<Rightarrow> o"  (infixl "\<in>" 50)  \<comment> \<open>membership relation\<close>
-  and zero :: "i"  ("0")  \<comment> \<open>the empty set\<close>
+axiomatization mem :: "[i, i] \<Rightarrow> o"  (infixl \<open>\<in>\<close> 50)  \<comment> \<open>membership relation\<close>
+  and zero :: "i"  (\<open>0\<close>)  \<comment> \<open>the empty set\<close>
   and Pow :: "i \<Rightarrow> i"  \<comment> \<open>power sets\<close>
   and Inf :: "i"  \<comment> \<open>infinite set\<close>
-  and Union :: "i \<Rightarrow> i"  ("\<Union>_" [90] 90)
+  and Union :: "i \<Rightarrow> i"  (\<open>\<Union>_\<close> [90] 90)
   and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
 
-abbreviation not_mem :: "[i, i] \<Rightarrow> o"  (infixl "\<notin>" 50)  \<comment> \<open>negated membership relation\<close>
+abbreviation not_mem :: "[i, i] \<Rightarrow> o"  (infixl \<open>\<notin>\<close> 50)  \<comment> \<open>negated membership relation\<close>
   where "x \<notin> y \<equiv> \<not> (x \<in> y)"
 
 
@@ -36,8 +36,8 @@
   where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)"
 
 syntax
-  "_Ball" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<forall>_\<in>_./ _)" 10)
-  "_Bex" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<exists>_\<in>_./ _)" 10)
+  "_Ball" :: "[pttrn, i, o] \<Rightarrow> o"  (\<open>(3\<forall>_\<in>_./ _)\<close> 10)
+  "_Bex" :: "[pttrn, i, o] \<Rightarrow> o"  (\<open>(3\<exists>_\<in>_./ _)\<close> 10)
 translations
   "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"
   "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"
@@ -52,7 +52,7 @@
   where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
 
 syntax
-  "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i"  (\<open>(1{_ ./ _ \<in> _, _})\<close>)
 translations
   "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
 
@@ -63,7 +63,7 @@
   where "RepFun(A,f) == {y . x\<in>A, y=f(x)}"
 
 syntax
-  "_RepFun" :: "[i, pttrn, i] => i"  ("(1{_ ./ _ \<in> _})" [51,0,51])
+  "_RepFun" :: "[i, pttrn, i] => i"  (\<open>(1{_ ./ _ \<in> _})\<close> [51,0,51])
 translations
   "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
 
@@ -74,19 +74,19 @@
   where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"
 
 syntax
-  "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  ("(1{_ \<in> _ ./ _})")
+  "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  (\<open>(1{_ \<in> _ ./ _})\<close>)
 translations
   "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
 
 
 subsection \<open>General union and intersection\<close>
 
-definition Inter :: "i => i"  ("\<Inter>_" [90] 90)
+definition Inter :: "i => i"  (\<open>\<Inter>_\<close> [90] 90)
   where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
 
 syntax
-  "_UNION" :: "[pttrn, i, i] => i"  ("(3\<Union>_\<in>_./ _)" 10)
-  "_INTER" :: "[pttrn, i, i] => i"  ("(3\<Inter>_\<in>_./ _)" 10)
+  "_UNION" :: "[pttrn, i, i] => i"  (\<open>(3\<Union>_\<in>_./ _)\<close> 10)
+  "_INTER" :: "[pttrn, i, i] => i"  (\<open>(3\<Inter>_\<in>_./ _)\<close> 10)
 translations
   "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
   "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
@@ -100,16 +100,16 @@
 definition Upair :: "[i, i] => i"
   where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
 
-definition Subset :: "[i, i] \<Rightarrow> o"  (infixl "\<subseteq>" 50)  \<comment> \<open>subset relation\<close>
+definition Subset :: "[i, i] \<Rightarrow> o"  (infixl \<open>\<subseteq>\<close> 50)  \<comment> \<open>subset relation\<close>
   where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B"
 
-definition Diff :: "[i, i] \<Rightarrow> i"  (infixl "-" 65)  \<comment> \<open>set difference\<close>
+definition Diff :: "[i, i] \<Rightarrow> i"  (infixl \<open>-\<close> 65)  \<comment> \<open>set difference\<close>
   where "A - B == { x\<in>A . ~(x\<in>B) }"
 
-definition Un :: "[i, i] \<Rightarrow> i"  (infixl "\<union>" 65)  \<comment> \<open>binary union\<close>
+definition Un :: "[i, i] \<Rightarrow> i"  (infixl \<open>\<union>\<close> 65)  \<comment> \<open>binary union\<close>
   where "A \<union> B == \<Union>(Upair(A,B))"
 
-definition Int :: "[i, i] \<Rightarrow> i"  (infixl "\<inter>" 70)  \<comment> \<open>binary intersection\<close>
+definition Int :: "[i, i] \<Rightarrow> i"  (infixl \<open>\<inter>\<close> 70)  \<comment> \<open>binary intersection\<close>
   where "A \<inter> B == \<Inter>(Upair(A,B))"
 
 definition cons :: "[i, i] => i"
@@ -120,9 +120,9 @@
 
 nonterminal "is"
 syntax
-  "" :: "i \<Rightarrow> is"  ("_")
-  "_Enum" :: "[i, is] \<Rightarrow> is"  ("_,/ _")
-  "_Finset" :: "is \<Rightarrow> i"  ("{(_)}")
+  "" :: "i \<Rightarrow> is"  (\<open>_\<close>)
+  "_Enum" :: "[i, is] \<Rightarrow> is"  (\<open>_,/ _\<close>)
+  "_Finset" :: "is \<Rightarrow> i"  (\<open>{(_)}\<close>)
 translations
   "{x, xs}" == "CONST cons(x, {xs})"
   "{x}" == "CONST cons(x, 0)"
@@ -153,14 +153,14 @@
 
 subsection \<open>Definite descriptions -- via Replace over the set "1"\<close>
 
-definition The :: "(i \<Rightarrow> o) \<Rightarrow> i"  (binder "THE " 10)
+definition The :: "(i \<Rightarrow> o) \<Rightarrow> i"  (binder \<open>THE \<close> 10)
   where the_def: "The(P)    == \<Union>({y . x \<in> {0}, P(y)})"
 
-definition If :: "[o, i, i] \<Rightarrow> i"  ("(if (_)/ then (_)/ else (_))" [10] 10)
+definition If :: "[o, i, i] \<Rightarrow> i"  (\<open>(if (_)/ then (_)/ else (_))\<close> [10] 10)
   where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b"
 
 abbreviation (input)
-  old_if :: "[o, i, i] => i"  ("if '(_,_,_')")
+  old_if :: "[o, i, i] => i"  (\<open>if '(_,_,_')\<close>)
   where "if(P,a,b) == If(P,a,b)"
 
 
@@ -182,10 +182,10 @@
 (* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
 nonterminal patterns
 syntax
-  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
-  ""          :: "pttrn => patterns"         ("_")
-  "_patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
-  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
+  "_pattern"  :: "patterns => pttrn"         (\<open>\<langle>_\<rangle>\<close>)
+  ""          :: "pttrn => patterns"         (\<open>_\<close>)
+  "_patterns" :: "[pttrn, patterns] => patterns"  (\<open>_,/_\<close>)
+  "_Tuple"    :: "[i, is] => i"              (\<open>\<langle>(_,/ _)\<rangle>\<close>)
 translations
   "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
@@ -195,7 +195,7 @@
 definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
   where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"
 
-abbreviation cart_prod :: "[i, i] => i"  (infixr "\<times>" 80)  \<comment> \<open>Cartesian product\<close>
+abbreviation cart_prod :: "[i, i] => i"  (infixr \<open>\<times>\<close> 80)  \<comment> \<open>Cartesian product\<close>
   where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"
 
 
@@ -220,10 +220,10 @@
 definition "function" :: "i \<Rightarrow> o"  \<comment> \<open>recognizes functions; can have non-pairs\<close>
   where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')"
 
-definition Image :: "[i, i] \<Rightarrow> i"  (infixl "``" 90)  \<comment> \<open>image\<close>
+definition Image :: "[i, i] \<Rightarrow> i"  (infixl \<open>``\<close> 90)  \<comment> \<open>image\<close>
   where image_def: "r `` A  == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}"
 
-definition vimage :: "[i, i] \<Rightarrow> i"  (infixl "-``" 90)  \<comment> \<open>inverse image\<close>
+definition vimage :: "[i, i] \<Rightarrow> i"  (infixl \<open>-``\<close> 90)  \<comment> \<open>inverse image\<close>
   where vimage_def: "r -`` A == converse(r)``A"
 
 (* Restrict the relation r to the domain A *)
@@ -236,22 +236,22 @@
 definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
   where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}"
 
-definition "apply" :: "[i, i] \<Rightarrow> i"  (infixl "`" 90)  \<comment> \<open>function application\<close>
+definition "apply" :: "[i, i] \<Rightarrow> i"  (infixl \<open>`\<close> 90)  \<comment> \<open>function application\<close>
   where "f`a == \<Union>(f``{a})"
 
 definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
   where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}"
 
-abbreviation function_space :: "[i, i] \<Rightarrow> i"  (infixr "->" 60)  \<comment> \<open>function space\<close>
+abbreviation function_space :: "[i, i] \<Rightarrow> i"  (infixr \<open>->\<close> 60)  \<comment> \<open>function space\<close>
   where "A -> B \<equiv> Pi(A, \<lambda>_. B)"
 
 
 (* binder syntax *)
 
 syntax
-  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Prod>_\<in>_./ _)" 10)
-  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sum>_\<in>_./ _)" 10)
-  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        (\<open>(3\<Prod>_\<in>_./ _)\<close> 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        (\<open>(3\<Sum>_\<in>_./ _)\<close> 10)
+  "_lam"      :: "[pttrn, i, i] => i"        (\<open>(3\<lambda>_\<in>_./ _)\<close> 10)
 translations
   "\<Prod>x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
   "\<Sum>x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"
@@ -261,27 +261,27 @@
 subsection \<open>ASCII syntax\<close>
 
 notation (ASCII)
-  cart_prod       (infixr "*" 80) and
-  Int             (infixl "Int" 70) and
-  Un              (infixl "Un" 65) and
-  function_space  (infixr "\<rightarrow>" 60) and
-  Subset          (infixl "<=" 50) and
-  mem             (infixl ":" 50) and
-  not_mem         (infixl "~:" 50)
+  cart_prod       (infixr \<open>*\<close> 80) and
+  Int             (infixl \<open>Int\<close> 70) and
+  Un              (infixl \<open>Un\<close> 65) and
+  function_space  (infixr \<open>\<rightarrow>\<close> 60) and
+  Subset          (infixl \<open><=\<close> 50) and
+  mem             (infixl \<open>:\<close> 50) and
+  not_mem         (infixl \<open>~:\<close> 50)
 
 syntax (ASCII)
-  "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
-  "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
-  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
-  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
-  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
-  "_UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
-  "_INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
-  "_PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
-  "_SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
-  "_lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
-  "_Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
-  "_pattern"  :: "patterns => pttrn"         ("<_>")
+  "_Ball"     :: "[pttrn, i, o] => o"        (\<open>(3ALL _:_./ _)\<close> 10)
+  "_Bex"      :: "[pttrn, i, o] => o"        (\<open>(3EX _:_./ _)\<close> 10)
+  "_Collect"  :: "[pttrn, i, o] => i"        (\<open>(1{_: _ ./ _})\<close>)
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i" (\<open>(1{_ ./ _: _, _})\<close>)
+  "_RepFun"   :: "[i, pttrn, i] => i"        (\<open>(1{_ ./ _: _})\<close> [51,0,51])
+  "_UNION"    :: "[pttrn, i, i] => i"        (\<open>(3UN _:_./ _)\<close> 10)
+  "_INTER"    :: "[pttrn, i, i] => i"        (\<open>(3INT _:_./ _)\<close> 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        (\<open>(3PROD _:_./ _)\<close> 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        (\<open>(3SUM _:_./ _)\<close> 10)
+  "_lam"      :: "[pttrn, i, i] => i"        (\<open>(3lam _:_./ _)\<close> 10)
+  "_Tuple"    :: "[i, is] => i"              (\<open><(_,/ _)>\<close>)
+  "_pattern"  :: "patterns => pttrn"         (\<open><_>\<close>)
 
 
 subsection \<open>Substitution\<close>
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/ex/Group.thy
--- a/src/ZF/ex/Group.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/ex/Group.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -22,11 +22,11 @@
   "carrier(M) == fst(M)"
 
 definition
-  mmult :: "[i, i, i] => i" (infixl "\<cdot>\<index>" 70) where
+  mmult :: "[i, i, i] => i" (infixl \<open>\<cdot>\<index>\<close> 70) where
   "mmult(M,x,y) == fst(snd(M)) ` <x,y>"
 
 definition
-  one :: "i => i" ("\<one>\<index>") where
+  one :: "i => i" (\<open>\<one>\<index>\<close>) where
   "one(M) == fst(snd(snd(M)))"
 
 definition
@@ -34,7 +34,7 @@
   "update_carrier(M,A) == <A,snd(M)>"
 
 definition
-  m_inv :: "i => i => i" ("inv\<index> _" [81] 80) where
+  m_inv :: "i => i => i" (\<open>inv\<index> _\<close> [81] 80) where
   "inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier(G) & y \<cdot>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> & x \<cdot>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub>)"
 
 locale monoid = fixes G (structure)
@@ -302,7 +302,7 @@
 subsection \<open>Direct Products\<close>
 
 definition
-  DirProdGroup :: "[i,i] => i"  (infixr "\<Otimes>" 80) where
+  DirProdGroup :: "[i,i] => i"  (infixr \<open>\<Otimes>\<close> 80) where
   "G \<Otimes> H == <carrier(G) \<times> carrier(H),
               (\<lambda><<g,h>, <g', h'>>
                    \<in> (carrier(G) \<times> carrier(H)) \<times> (carrier(G) \<times> carrier(H)).
@@ -370,7 +370,7 @@
 subsection \<open>Isomorphisms\<close>
 
 definition
-  iso :: "[i,i] => i"  (infixr "\<cong>" 60) where
+  iso :: "[i,i] => i"  (infixr \<open>\<cong>\<close> 60) where
   "G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))"
 
 lemma (in group) iso_refl: "id(carrier(G)) \<in> G \<cong> G"
@@ -576,23 +576,23 @@
 subsection\<open>Cosets and Quotient Groups\<close>
 
 definition
-  r_coset  :: "[i,i,i] => i"  (infixl "#>\<index>" 60) where
+  r_coset  :: "[i,i,i] => i"  (infixl \<open>#>\<index>\<close> 60) where
   "H #>\<^bsub>G\<^esub> a == \<Union>h\<in>H. {h \<cdot>\<^bsub>G\<^esub> a}"
 
 definition
-  l_coset  :: "[i,i,i] => i"  (infixl "<#\<index>" 60) where
+  l_coset  :: "[i,i,i] => i"  (infixl \<open><#\<index>\<close> 60) where
   "a <#\<^bsub>G\<^esub> H == \<Union>h\<in>H. {a \<cdot>\<^bsub>G\<^esub> h}"
 
 definition
-  RCOSETS  :: "[i,i] => i"  ("rcosets\<index> _" [81] 80) where
+  RCOSETS  :: "[i,i] => i"  (\<open>rcosets\<index> _\<close> [81] 80) where
   "rcosets\<^bsub>G\<^esub> H == \<Union>a\<in>carrier(G). {H #>\<^bsub>G\<^esub> a}"
 
 definition
-  set_mult :: "[i,i,i] => i"  (infixl "<#>\<index>" 60) where
+  set_mult :: "[i,i,i] => i"  (infixl \<open><#>\<index>\<close> 60) where
   "H <#>\<^bsub>G\<^esub> K == \<Union>h\<in>H. \<Union>k\<in>K. {h \<cdot>\<^bsub>G\<^esub> k}"
 
 definition
-  SET_INV  :: "[i,i] => i"  ("set'_inv\<index> _" [81] 80) where
+  SET_INV  :: "[i,i] => i"  (\<open>set'_inv\<index> _\<close> [81] 80) where
   "set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
 
 
@@ -600,7 +600,7 @@
   assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"
 
 notation
-  normal  (infixl "\<lhd>" 60)
+  normal  (infixl \<open>\<lhd>\<close> 60)
 
 
 subsection \<open>Basic Properties of Cosets\<close>
@@ -860,7 +860,7 @@
 subsubsection\<open>Two distinct right cosets are disjoint\<close>
 
 definition
-  r_congruent :: "[i,i] => i" ("rcong\<index> _" [60] 60) where
+  r_congruent :: "[i,i] => i" (\<open>rcong\<index> _\<close> [60] 60) where
   "rcong\<^bsub>G\<^esub> H == {<x,y> \<in> carrier(G) * carrier(G). inv\<^bsub>G\<^esub> x \<cdot>\<^bsub>G\<^esub> y \<in> H}"
 
 
@@ -1020,7 +1020,7 @@
 subsection \<open>Quotient Groups: Factorization of a Group\<close>
 
 definition
-  FactGroup :: "[i,i] => i" (infixl "Mod" 65) where
+  FactGroup :: "[i,i] => i" (infixl \<open>Mod\<close> 65) where
     \<comment> \<open>Actually defined for groups rather than monoids\<close>
   "G Mod H ==
      <rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#>\<^bsub>G\<^esub> K2, H, 0>"
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/ex/Primes.thy
--- a/src/ZF/ex/Primes.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/ex/Primes.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -8,7 +8,7 @@
 theory Primes imports ZF begin
 
 definition
-  divides :: "[i,i]=>o"              (infixl "dvd" 50)  where
+  divides :: "[i,i]=>o"              (infixl \<open>dvd\<close> 50)  where
     "m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
 
 definition
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/ex/Ring.thy
--- a/src/ZF/ex/Ring.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/ex/Ring.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -7,8 +7,8 @@
 theory Ring imports Group begin
 
 no_notation
-  cadd  (infixl "\<oplus>" 65) and
-  cmult  (infixl "\<otimes>" 70)
+  cadd  (infixl \<open>\<oplus>\<close> 65) and
+  cmult  (infixl \<open>\<otimes>\<close> 70)
 
 (*First, we must simulate a record declaration:
 record ring = monoid +
@@ -21,11 +21,11 @@
   "add_field(M) = fst(snd(snd(snd(M))))"
 
 definition
-  ring_add :: "[i, i, i] => i" (infixl "\<oplus>\<index>" 65) where
+  ring_add :: "[i, i, i] => i" (infixl \<open>\<oplus>\<index>\<close> 65) where
   "ring_add(M,x,y) = add_field(M) ` <x,y>"
 
 definition
-  zero :: "i => i" ("\<zero>\<index>") where
+  zero :: "i => i" (\<open>\<zero>\<index>\<close>) where
   "zero(M) = fst(snd(snd(snd(snd(M)))))"
 
 
@@ -42,11 +42,11 @@
 text \<open>Derived operations.\<close>
 
 definition
-  a_inv :: "[i,i] => i" ("\<ominus>\<index> _" [81] 80) where
+  a_inv :: "[i,i] => i" (\<open>\<ominus>\<index> _\<close> [81] 80) where
   "a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"
 
 definition
-  minus :: "[i,i,i] => i" ("(_ \<ominus>\<index> _)" [65,66] 65) where
+  minus :: "[i,i,i] => i" (\<open>(_ \<ominus>\<index> _)\<close> [65,66] 65) where
   "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
 
 locale abelian_monoid = fixes G (structure)
diff -r 9171d1ce5a35 -r 53982d5ec0bb src/ZF/func.thy
--- a/src/ZF/func.thy	Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/func.thy	Thu Jan 03 21:15:52 2019 +0100
@@ -451,10 +451,10 @@
 
   (* Let expressions *)
 
-  "_updbind"    :: "[i, i] => updbind"               ("(2_ :=/ _)")
-  ""            :: "updbind => updbinds"             ("_")
-  "_updbinds"   :: "[updbind, updbinds] => updbinds" ("_,/ _")
-  "_Update"     :: "[i, updbinds] => i"              ("_/'((_)')" [900,0] 900)
+  "_updbind"    :: "[i, i] => updbind"               (\<open>(2_ :=/ _)\<close>)
+  ""            :: "updbind => updbinds"             (\<open>_\<close>)
+  "_updbinds"   :: "[updbind, updbinds] => updbinds" (\<open>_,/ _\<close>)
+  "_Update"     :: "[i, updbinds] => i"              (\<open>_/'((_)')\<close> [900,0] 900)
 
 translations
   "_Update (f, _updbinds(b,bs))"  == "_Update (_Update(f,b), bs)"