# HG changeset patch
# User haftmann
# Date 1228294438 -3600
# Node ID 1860f016886d3fdad5873e2ca985fccbaad50341
# Parent  ac1a14b5a0853d7a6d118dc8f81fc3c2166d14ba
fixed typo

diff -r ac1a14b5a085 -r 1860f016886d doc-src/IsarAdvanced/Classes/Thy/Classes.thy
--- 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"} \\
diff -r ac1a14b5a085 -r 1860f016886d doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- 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} \\