tuned -- avoid conflict with cartouche argument;
authorwenzelm
Wed, 26 Dec 2018 16:07:28 +0100
changeset 69504 bda7527ccf05
parent 69503 c2a736883b01
child 69505 cc2d676d5395
tuned -- avoid conflict with cartouche argument;
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"} \\