--- a/doc-src/AxClass/generated/Product.tex Fri Aug 04 10:59:22 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex Fri Aug 04 10:59:28 2000 +0200
@@ -1,7 +1,7 @@
\begin{isabelle}%
%
\isamarkupheader{Syntactic classes}
-\isacommand{theory}~Product~=~Main:%
+\isacommand{theory}\ Product\ =\ Main:%
\begin{isamarkuptext}%
\medskip\noindent There is still a feature of Isabelle's type system
left that we have not yet discussed. When declaring polymorphic
@@ -17,9 +17,9 @@
syntactic type classes.%
\end{isamarkuptext}%
\isacommand{axclass}\isanewline
-~~product~<~{"}term{"}\isanewline
+\ \ product\ <\ {"}term{"}\isanewline
\isacommand{consts}\isanewline
-~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)%
+\ \ product\ ::\ {"}'a::product\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)%
\begin{isamarkuptext}%
Here class $product$ is defined as subclass of $term$ without any
additional axioms. This effects in logical equivalence of $product$
@@ -48,10 +48,10 @@
This is done for class $product$ and type $bool$ as follows.%
\end{isamarkuptext}%
-\isacommand{instance}~bool~::~product\isanewline
-~~\isacommand{by}~intro\_classes\isanewline
-\isacommand{defs}~(\isakeyword{overloaded})\isanewline
-~~product\_bool\_def:~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}%
+\isacommand{instance}\ bool\ ::\ product\isanewline
+\ \ \isacommand{by}\ intro\_classes\isanewline
+\isacommand{defs}\ (\isakeyword{overloaded})\isanewline
+\ \ product\_bool\_def:\ {"}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{"}%
\begin{isamarkuptext}%
The definition $prod_bool_def$ becomes syntactically well-formed only
after the arity $bool :: product$ is made known to the type checker.