--- a/doc-src/TutorialI/Types/document/Axioms.tex Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Tue Oct 31 08:53:12 2000 +0100
@@ -59,7 +59,6 @@
This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms,
specialized to type \isa{bool}, as subgoals:
\begin{isabelle}%
-OFCLASS{\isacharparenleft}bool{\isacharcomma}\ parord{\isacharunderscore}class{\isacharparenright}\isanewline
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}\ z{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z\isanewline
\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline