--- a/doc-src/AxClass/generated/Group.tex Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex Sun Oct 15 19:51:56 2000 +0200
@@ -180,8 +180,8 @@
\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
-\medskip The $\isakeyword{instance}$ command sets up an appropriate
- goal that represents the class inclusion (or type arity, see
+\medskip The $\INSTANCE$ command sets up an appropriate goal that
+ represents the class inclusion (or type arity, see
\secref{sec:inst-arity}) to be proven (see also
\cite{isabelle-isar-ref}). The \isa{intro{\isacharunderscore}classes} proof method
does back-chaining of class membership statements wrt.\ the hierarchy
@@ -194,14 +194,14 @@
\isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}}
%
\begin{isamarkuptext}%
-So far we have covered the case of the form
- $\isakeyword{instance}~c@1 < c@2$, namely \emph{abstract
- instantiation} --- $c@1$ is more special than $c@2$ and thus an
- instance of $c@2$. Even more interesting for practical applications
- are \emph{concrete instantiations} of axiomatic type classes. That
- is, certain simple schemes $(\alpha@1, \ldots, \alpha@n)t :: c$ of
- class membership may be established at the logical level and then
- transferred to Isabelle's type signature level.
+So far we have covered the case of the form $\INSTANCE$~\isa{c\isactrlsub {\isadigit{1}}\ {\isacharless}\ c\isactrlsub {\isadigit{2}}}, namely \emph{abstract instantiation} ---
+ $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance
+ of \isa{c\isactrlsub {\isadigit{2}}}. Even more interesting for practical
+ applications are \emph{concrete instantiations} of axiomatic type
+ classes. That is, certain simple schemes
+ \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of class membership may be
+ established at the logical level and then transferred to Isabelle's
+ type signature level.
\medskip As a typical example, we show that type \isa{bool} with
exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
@@ -235,10 +235,10 @@
\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
-The result of an $\isakeyword{instance}$ statement is both expressed
- as a theorem of Isabelle's meta-logic, and as a type arity of the
- type signature. The latter enables type-inference system to take
- care of this new instance automatically.
+The result of an $\INSTANCE$ statement is both expressed as a theorem
+ of Isabelle's meta-logic, and as a type arity of the type signature.
+ The latter enables type-inference system to take care of this new
+ instance automatically.
\medskip We could now also instantiate our group theory classes to
many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup}
@@ -255,9 +255,9 @@
\begin{isamarkuptext}%
As already mentioned above, overloading in the simply-typed HOL
systems may include recursion over the syntactic structure of types.
- That is, definitional equations $c^\tau \equiv t$ may also contain
- constants of name $c$ on the right-hand side --- if these have types
- that are structurally simpler than $\tau$.
+ That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also
+ contain constants of name \isa{c} on the right-hand side --- if
+ these have types that are structurally simpler than \isa{{\isasymtau}}.
This feature enables us to \emph{lift operations}, say to Cartesian
products, direct sums or function spaces. Subsequently we lift