diff -r 9fa7d3890488 -r ba9297b71897 doc-src/AxClass/generated/Product.tex
--- a/doc-src/AxClass/generated/Product.tex	Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex	Tue Oct 03 18:55:23 2000 +0200
@@ -7,63 +7,66 @@
 \begin{isamarkuptext}%
 \medskip\noindent There is still a feature of Isabelle's type system
  left that we have not yet discussed.  When declaring polymorphic
- constants $c :: \sigma$, the type variables occurring in $\sigma$ may
- be constrained by type classes (or even general sorts) in an
+ constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}}
+ may be constrained by type classes (or even general sorts) in an
  arbitrary way.  Note that by default, in Isabelle/HOL the declaration
- $\TIMES :: \alpha \To \alpha \To \alpha$ is actually an abbreviation
- for $\TIMES :: (\alpha::term) \To \alpha \To \alpha$.  Since class
- $term$ is the universal class of HOL, this is not really a constraint
- at all.
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation for
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}term\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{term} is the
+ universal class of HOL, this is not really a constraint at all.
 
- The $product$ class below provides a less degenerate example of
+ The \isa{product} class below provides a less degenerate example of
  syntactic type classes.%
 \end{isamarkuptext}%
 \isacommand{axclass}\isanewline
 \ \ product\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
 \isacommand{consts}\isanewline
-\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isacharcolon}{\isacharcolon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}%
+\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}%
 \begin{isamarkuptext}%
-Here class $product$ is defined as subclass of $term$ without any
- additional axioms.  This effects in logical equivalence of $product$
- and $term$, as is reflected by the trivial introduction rule
- generated for this definition.
+Here class \isa{product} is defined as subclass of \isa{term}
+ without any additional axioms.  This effects in logical equivalence
+ of \isa{product} and \isa{term}, as is reflected by the trivial
+ introduction rule generated for this definition.
 
- \medskip So what is the difference of declaring $\TIMES :: (\alpha ::
- product) \To \alpha \To \alpha$ vs.\ declaring $\TIMES :: (\alpha ::
- term) \To \alpha \To \alpha$ anyway?  In this particular case where
- $product \equiv term$, it should be obvious that both declarations
- are the same from the logic's point of view.  It even makes the most
- sense to remove sort constraints from constant declarations, as far
- as the purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
+ \medskip So what is the difference of declaring
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} vs.\ declaring
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}term\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} anyway?  In this particular case
+ where \isa{product\ {\isasymequiv}\ term}, it should be obvious that both
+ declarations are the same from the logic's point of view.  It even
+ makes the most sense to remove sort constraints from constant
+ declarations, as far as the purely logical meaning is concerned
+ \cite{Wenzel:1997:TPHOL}.
 
  On the other hand there are syntactic differences, of course.
- Constants $\TIMES^\tau$ are rejected by the type-checker, unless the
- arity $\tau :: product$ is part of the type signature.  In our
- example, this arity may be always added when required by means of an
- $\isarkeyword{instance}$ with the trivial proof $\BY{intro_classes}$.
+ Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
+ type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
+ type signature.  In our example, this arity may be always added when
+ required by means of an $\isarkeyword{instance}$ with the trivial
+ proof $\BY{intro_classes}$.
 
  \medskip Thus, we may observe the following discipline of using
  syntactic classes.  Overloaded polymorphic constants have their type
- arguments restricted to an associated (logically trivial) class $c$.
- Only immediately before \emph{specifying} these constants on a
- certain type $\tau$ do we instantiate $\tau :: c$.
+ arguments restricted to an associated (logically trivial) class
+ \isa{c}.  Only immediately before \emph{specifying} these constants
+ on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}.
 
- This is done for class $product$ and type $bool$ as follows.%
+ This is done for class \isa{product} and type \isa{bool} as
+ follows.%
 \end{isamarkuptext}%
 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\isanewline
 \ \ \isacommand{by}\ intro{\isacharunderscore}classes\isanewline
 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}%
+\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}%
 \begin{isamarkuptext}%
-The definition $prod_bool_def$ becomes syntactically well-formed only
- after the arity $bool :: product$ is made known to the type checker.
+The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically
+ well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made
+ known to the type checker.
 
  \medskip It is very important to see that above $\DEFS$ are not
  directly connected with $\isarkeyword{instance}$ at all!  We were
- just following our convention to specify $\TIMES$ on $bool$ after
- having instantiated $bool :: product$.  Isabelle does not require
- these definitions, which is in contrast to programming languages like
- Haskell \cite{haskell-report}.
+ just following our convention to specify \isa{{\isasymodot}} on \isa{bool}
+ after having instantiated \isa{bool\ {\isasymColon}\ product}.  Isabelle does
+ not require these definitions, which is in contrast to programming
+ languages like Haskell \cite{haskell-report}.
 
  \medskip While Isabelle type classes and those of Haskell are almost
  the same as far as type-checking and type inference are concerned,
@@ -72,9 +75,9 @@
  Therefore, its \texttt{instance} has a \texttt{where} part that tells
  the system what these ``member functions'' should be.
 
- This style of \texttt{instance} won't make much sense in Isabelle's
- meta-logic, because there is no internal notion of ``providing
- operations'' or even ``names of functions''.%
+ This style of \texttt{instance} would not make much sense in
+ Isabelle's meta-logic, because there is no internal notion of
+ ``providing operations'' or even ``names of functions''.%
 \end{isamarkuptext}%
 \isacommand{end}\end{isabellebody}%
 %%% Local Variables: