diff -r 3032bc7d613d -r d052d61da398 src/Doc/Classes/Classes.thy
--- a/src/Doc/Classes/Classes.thy	Tue Sep 12 13:54:48 2023 +0100
+++ b/src/Doc/Classes/Classes.thy	Wed Sep 13 17:08:54 2023 +0000
@@ -101,8 +101,8 @@
 \<close>
 
 class %quote semigroup =
-  fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<otimes>" 70)
-  assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
+  fixes mult :: \<open>\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>\<close>   (infixl \<open>\<otimes>\<close> 70)
+  assumes assoc: \<open>(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)\<close>
 
 text \<open>
   \<^noindent> This @{command class} specification consists of two parts:
@@ -110,9 +110,9 @@
   "fixes"}), the \qn{logical} part specifies properties on them
   (@{element "assumes"}).  The local @{element "fixes"} and @{element
   "assumes"} are lifted to the theory toplevel, yielding the global
-  parameter @{term [source] "mult :: \<alpha>::semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
-  global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y z ::
-  \<alpha>::semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
+  parameter @{term [source] \<open>mult :: \<alpha>::semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>\<close>} and the
+  global theorem @{fact "semigroup.assoc:"}~@{prop [source] \<open>\<And>x y z ::
+  \<alpha>::semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)\<close>}.
 \<close>
 
 
@@ -128,11 +128,11 @@
 begin
 
 definition %quote
-  mult_int_def: "i \<otimes> j = i + (j::int)"
+  mult_int_def: \<open>i \<otimes> j = i + (j::int)\<close>
 
 instance %quote proof
-  fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
-  then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
+  fix i j k :: int have \<open>(i + j) + k = i + (j + k)\<close> by simp
+  then show \<open>(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)\<close>
     unfolding mult_int_def .
 qed
 
@@ -160,12 +160,12 @@
 begin
 
 primrec %quote mult_nat where
-  "(0::nat) \<otimes> n = n"
-  | "Suc m \<otimes> n = Suc (m \<otimes> n)"
+  \<open>(0::nat) \<otimes> n = n\<close>
+  | \<open>Suc m \<otimes> n = Suc (m \<otimes> n)\<close>
 
 instance %quote proof
   fix m n q :: nat 
-  show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
+  show \<open>m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)\<close>
     by (induct m) auto
 qed
 
@@ -191,11 +191,11 @@
 begin
 
 definition %quote
-  mult_prod_def: "p\<^sub>1 \<otimes> p\<^sub>2 = (fst p\<^sub>1 \<otimes> fst p\<^sub>2, snd p\<^sub>1 \<otimes> snd p\<^sub>2)"
+  mult_prod_def: \<open>p\<^sub>1 \<otimes> p\<^sub>2 = (fst p\<^sub>1 \<otimes> fst p\<^sub>2, snd p\<^sub>1 \<otimes> snd p\<^sub>2)\<close>
 
 instance %quote proof
-  fix p\<^sub>1 p\<^sub>2 p\<^sub>3 :: "\<alpha>::semigroup \<times> \<beta>::semigroup"
-  show "p\<^sub>1 \<otimes> p\<^sub>2 \<otimes> p\<^sub>3 = p\<^sub>1 \<otimes> (p\<^sub>2 \<otimes> p\<^sub>3)"
+  fix p\<^sub>1 p\<^sub>2 p\<^sub>3 :: \<open>\<alpha>::semigroup \<times> \<beta>::semigroup\<close>
+  show \<open>p\<^sub>1 \<otimes> p\<^sub>2 \<otimes> p\<^sub>3 = p\<^sub>1 \<otimes> (p\<^sub>2 \<otimes> p\<^sub>3)\<close>
     unfolding mult_prod_def by (simp add: assoc)
 qed      
 
@@ -220,8 +220,8 @@
 \<close>
 
 class %quote monoidl = semigroup +
-  fixes neutral :: "\<alpha>" ("\<one>")
-  assumes neutl: "\<one> \<otimes> x = x"
+  fixes neutral :: \<open>\<alpha>\<close> (\<open>\<one>\<close>)
+  assumes neutl: \<open>\<one> \<otimes> x = x\<close>
 
 text \<open>
   \<^noindent> Again, we prove some instances, by providing suitable
@@ -234,18 +234,18 @@
 begin
 
 definition %quote
-  neutral_nat_def: "\<one> = (0::nat)"
+  neutral_nat_def: \<open>\<one> = (0::nat)\<close>
 
 definition %quote
-  neutral_int_def: "\<one> = (0::int)"
+  neutral_int_def: \<open>\<one> = (0::int)\<close>
 
 instance %quote proof
   fix n :: nat
-  show "\<one> \<otimes> n = n"
+  show \<open>\<one> \<otimes> n = n\<close>
     unfolding neutral_nat_def by simp
 next
   fix k :: int
-  show "\<one> \<otimes> k = k"
+  show \<open>\<one> \<otimes> k = k\<close>
     unfolding neutral_int_def mult_int_def by simp
 qed
 
@@ -255,11 +255,11 @@
 begin
 
 definition %quote
-  neutral_prod_def: "\<one> = (\<one>, \<one>)"
+  neutral_prod_def: \<open>\<one> = (\<one>, \<one>)\<close>
 
 instance %quote proof
-  fix p :: "\<alpha>::monoidl \<times> \<beta>::monoidl"
-  show "\<one> \<otimes> p = p"
+  fix p :: \<open>\<alpha>::monoidl \<times> \<beta>::monoidl\<close>
+  show \<open>\<one> \<otimes> p = p\<close>
     unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
 qed
 
@@ -271,18 +271,18 @@
 \<close>
 
 class %quote monoid = monoidl +
-  assumes neutr: "x \<otimes> \<one> = x"
+  assumes neutr: \<open>x \<otimes> \<one> = x\<close>
 
 instantiation %quote nat and int :: monoid 
 begin
 
 instance %quote proof
   fix n :: nat
-  show "n \<otimes> \<one> = n"
+  show \<open>n \<otimes> \<one> = n\<close>
     unfolding neutral_nat_def by (induct n) simp_all
 next
   fix k :: int
-  show "k \<otimes> \<one> = k"
+  show \<open>k \<otimes> \<one> = k\<close>
     unfolding neutral_int_def mult_int_def by simp
 qed
 
@@ -292,8 +292,8 @@
 begin
 
 instance %quote proof 
-  fix p :: "\<alpha>::monoid \<times> \<beta>::monoid"
-  show "p \<otimes> \<one> = p"
+  fix p :: \<open>\<alpha>::monoid \<times> \<beta>::monoid\<close>
+  show \<open>p \<otimes> \<one> = p\<close>
     unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
 qed
 
@@ -304,19 +304,19 @@
 \<close>
 
 class %quote group = monoidl +
-  fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>"    ("(_\<div>)" [1000] 999)
-  assumes invl: "x\<div> \<otimes> x = \<one>"
+  fixes inverse :: \<open>\<alpha> \<Rightarrow> \<alpha>\<close>    (\<open>(_\<div>)\<close> [1000] 999)
+  assumes invl: \<open>x\<div> \<otimes> x = \<one>\<close>
 
 instantiation %quote int :: group
 begin
 
 definition %quote
-  inverse_int_def: "i\<div> = - (i::int)"
+  inverse_int_def: \<open>i\<div> = - (i::int)\<close>
 
 instance %quote proof
   fix i :: int
-  have "-i + i = 0" by simp
-  then show "i\<div> \<otimes> i = \<one>"
+  have \<open>-i + i = 0\<close> by simp
+  then show \<open>i\<div> \<otimes> i = \<one>\<close>
     unfolding mult_int_def neutral_int_def inverse_int_def .
 qed
 
@@ -335,20 +335,20 @@
 \<close>
 
 class %quote idem =
-  fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
-  assumes idem: "f (f x) = f x"
+  fixes f :: \<open>\<alpha> \<Rightarrow> \<alpha>\<close>
+  assumes idem: \<open>f (f x) = f x\<close>
 
 text \<open>
   \<^noindent> essentially introduces the locale
 \<close> (*<*)setup %invisible \<open>Sign.add_path "foo"\<close>
 (*>*)
 locale %quote idem =
-  fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
-  assumes idem: "f (f x) = f x"
+  fixes f :: \<open>\<alpha> \<Rightarrow> \<alpha>\<close>
+  assumes idem: \<open>f (f x) = f x\<close>
 
 text \<open>\<^noindent> together with corresponding constant(s):\<close>
 
-consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
+consts %quote f :: \<open>\<alpha> \<Rightarrow> \<alpha>\<close>
 
 text \<open>
   \<^noindent> The connection to the type system is done by means of a
@@ -357,7 +357,7 @@
 \<close>
 
 interpretation %quote idem_class:
-  idem "f :: (\<alpha>::idem) \<Rightarrow> \<alpha>"
+  idem \<open>f :: (\<alpha>::idem) \<Rightarrow> \<alpha>\<close>
 (*<*)sorry(*>*)
 
 text \<open>
@@ -375,26 +375,26 @@
   states that the function \<open>(x \<otimes>)\<close> is injective:
 \<close>
 
-lemma %quote (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
+lemma %quote (in group) left_cancel: \<open>x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z\<close>
 proof
-  assume "x \<otimes> y = x \<otimes> z"
-  then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
-  then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
-  then show "y = z" using neutl and invl by simp
+  assume \<open>x \<otimes> y = x \<otimes> z\<close>
+  then have \<open>x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)\<close> by simp
+  then have \<open>(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z\<close> using assoc by simp
+  then show \<open>y = z\<close> using neutl and invl by simp
 next
-  assume "y = z"
-  then show "x \<otimes> y = x \<otimes> z" by simp
+  assume \<open>y = z\<close>
+  then show \<open>x \<otimes> y = x \<otimes> z\<close> by simp
 qed
 
 text \<open>
   \<^noindent> Here the \qt{@{keyword "in"} \<^class>\<open>group\<close>} target
   specification indicates that the result is recorded within that
   context for later use.  This local theorem is also lifted to the
-  global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z ::
-  \<alpha>::group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.  Since type \<open>int\<close> has been
+  global one @{fact "group.left_cancel:"} @{prop [source] \<open>\<And>x y z ::
+  \<alpha>::group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z\<close>}.  Since type \<open>int\<close> has been
   made an instance of \<open>group\<close> before, we may refer to that
-  fact as well: @{prop [source] "\<And>x y z :: int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y =
-  z"}.
+  fact as well: @{prop [source] \<open>\<And>x y z :: int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y =
+  z\<close>}.
 \<close>
 
 
@@ -404,14 +404,14 @@
   Isabelle locales are targets which support local definitions:
 \<close>
 
-primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
-  "pow_nat 0 x = \<one>"
-  | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
+primrec %quote (in monoid) pow_nat :: \<open>nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>\<close> where
+  \<open>pow_nat 0 x = \<one>\<close>
+  | \<open>pow_nat (Suc n) x = x \<otimes> pow_nat n x\<close>
 
 text \<open>
   \<^noindent> If the locale \<open>group\<close> is also a class, this local
   definition is propagated onto a global definition of @{term [source]
-  "pow_nat :: nat \<Rightarrow> \<alpha>::monoid \<Rightarrow> \<alpha>::monoid"} with corresponding theorems
+  \<open>pow_nat :: nat \<Rightarrow> \<alpha>::monoid \<Rightarrow> \<alpha>::monoid\<close>} with corresponding theorems
 
   @{thm pow_nat.simps [no_vars]}.
 
@@ -438,7 +438,7 @@
   for lists:
 \<close>
 
-interpretation %quote list_monoid: monoid append "[]"
+interpretation %quote list_monoid: monoid append \<open>[]\<close>
   proof qed auto
 
 text \<open>
@@ -449,18 +449,18 @@
   be appropriate to map derived definitions accordingly:
 \<close>
 
-primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
-  "replicate 0 _ = []"
-  | "replicate (Suc n) xs = xs @ replicate n xs"
+primrec %quote replicate :: \<open>nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list\<close> where
+  \<open>replicate 0 _ = []\<close>
+  | \<open>replicate (Suc n) xs = xs @ replicate n xs\<close>
 
-interpretation %quote list_monoid: monoid append "[]" rewrites
-  "monoid.pow_nat append [] = replicate"
+interpretation %quote list_monoid: monoid append \<open>[]\<close> rewrites
+  \<open>monoid.pow_nat append [] = replicate\<close>
 proof -
-  interpret monoid append "[]" ..
-  show "monoid.pow_nat append [] = replicate"
+  interpret monoid append \<open>[]\<close> ..
+  show \<open>monoid.pow_nat append [] = replicate\<close>
   proof
     fix n
-    show "monoid.pow_nat append [] n = replicate n"
+    show \<open>monoid.pow_nat append [] n = replicate n\<close>
       by (induct n) auto
   qed
 qed intro_locales
@@ -486,9 +486,9 @@
 subclass %quote (in group) monoid
 proof
   fix x
-  from invl have "x\<div> \<otimes> x = \<one>" by simp
-  with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp
-  with left_cancel show "x \<otimes> \<one> = x" by simp
+  from invl have \<open>x\<div> \<otimes> x = \<one>\<close> by simp
+  with assoc [symmetric] neutl invl have \<open>x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x\<close> by simp
+  with left_cancel show \<open>x \<otimes> \<one> = x\<close> by simp
 qed
 
 text \<open>
@@ -530,14 +530,14 @@
   For illustration, a derived definition in \<open>group\<close> using \<open>pow_nat\<close>
 \<close>
 
-definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
-  "pow_int k x = (if k >= 0
+definition %quote (in group) pow_int :: \<open>int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>\<close> where
+  \<open>pow_int k x = (if k \<ge> 0
     then pow_nat (nat k) x
-    else (pow_nat (nat (- k)) x)\<div>)"
+    else (pow_nat (nat (- k)) x)\<div>)\<close>
 
 text \<open>
-  \<^noindent> yields the global definition of @{term [source] "pow_int ::
-  int \<Rightarrow> \<alpha>::group \<Rightarrow> \<alpha>::group"} with the corresponding theorem @{thm
+  \<^noindent> yields the global definition of @{term [source] \<open>pow_int ::
+  int \<Rightarrow> \<alpha>::group \<Rightarrow> \<alpha>::group\<close>} with the corresponding theorem @{thm
   pow_int_def [no_vars]}.
 \<close>
 
@@ -552,12 +552,12 @@
 context %quote semigroup
 begin
 
-term %quote "x \<otimes> y" \<comment> \<open>example 1\<close>
-term %quote "(x::nat) \<otimes> y" \<comment> \<open>example 2\<close>
+term %quote \<open>x \<otimes> y\<close> \<comment> \<open>example 1\<close>
+term %quote \<open>(x::nat) \<otimes> y\<close> \<comment> \<open>example 2\<close>
 
 end  %quote
 
-term %quote "x \<otimes> y" \<comment> \<open>example 3\<close>
+term %quote \<open>x \<otimes> y\<close> \<comment> \<open>example 3\<close>
 
 text \<open>
   \<^noindent> Here in example 1, the term refers to the local class
@@ -583,7 +583,7 @@
 \<close>
 
 definition %quote example :: int where
-  "example = pow_int 10 (-2)"
+  \<open>example = pow_int 10 (-2)\<close>
 
 text \<open>
   \<^noindent> This maps to Haskell as follows:
@@ -628,4 +628,3 @@
 \<close>
 
 end
-