doc-src/IsarAdvanced/Classes/Thy/Classes.thy
changeset 28948 1860f016886d
parent 28947 ac1a14b5a085
child 29294 6cd3ac4708d2
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Wed Dec 03 09:51:35 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Wed Dec 03 09:53:58 2008 +0100
@@ -29,7 +29,7 @@
   \hspace*{2ex}@{text "eq _ 0 = False"} \\
   \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
 
-  \medskip\noindent\@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
+  \medskip\noindent@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> 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"} \\