# HG changeset patch
# User wenzelm
# Date 1545836848 -3600
# Node ID bda7527ccf05e5b0a65726cce7c13d36c3868ba1
# Parent  c2a736883b018ba0e301fdbe1ffe883c64b62f1a
tuned -- avoid conflict with cartouche argument;

diff -r c2a736883b01 -r bda7527ccf05 src/Doc/Classes/Classes.thy
--- a/src/Doc/Classes/Classes.thy	Wed Dec 26 15:28:23 2018 +0100
+++ b/src/Doc/Classes/Classes.thy	Wed Dec 26 16:07:28 2018 +0100
@@ -19,19 +19,19 @@
 
   \begin{quote}
 
-  \<^noindent>@{text "class eq where"} \\
+  \<^noindent> @{text "class eq where"} \\
   \hspace*{2ex}@{text "eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
 
-  \<^medskip>\<^noindent>@{text "instance nat :: eq where"} \\
+  \<^medskip>\<^noindent> @{text "instance nat :: eq where"} \\
   \hspace*{2ex}@{text "eq 0 0 = True"} \\
   \hspace*{2ex}@{text "eq 0 _ = False"} \\
   \hspace*{2ex}@{text "eq _ 0 = False"} \\
   \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
 
-  \<^medskip>\<^noindent>@{text "instance (\<alpha>::eq, \<beta>::eq) pair :: eq where"} \\
+  \<^medskip>\<^noindent> @{text "instance (\<alpha>::eq, \<beta>::eq) pair :: eq where"} \\
   \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
 
-  \<^medskip>\<^noindent>@{text "class ord extends eq where"} \\
+  \<^medskip>\<^noindent> @{text "class ord extends eq where"} \\
   \hspace*{2ex}@{text "less_eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
   \hspace*{2ex}@{text "less :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
 
@@ -56,7 +56,7 @@
 
   \begin{quote}
 
-  \<^noindent>@{text "class eq where"} \\
+  \<^noindent> @{text "class eq where"} \\
   \hspace*{2ex}@{text "eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
   @{text "satisfying"} \\
   \hspace*{2ex}@{text "refl: eq x x"} \\