--- 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"} \\
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Dec 03 09:51:35 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Dec 03 09:53:58 2008 +0100
@@ -49,7 +49,7 @@
\hspace*{2ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
\hspace*{2ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
- \medskip\noindent\\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
+ \medskip\noindent\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
\hspace*{2ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
\medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\