updated;

--- a/doc-src/AxClass/generated/Group.tex	Mon Oct 23 22:10:36 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex	Mon Oct 23 22:11:24 2000 +0200
@@ -163,14 +163,14 @@
  \end{figure}%
 \end{isamarkuptext}%
 \isacommand{instance}\ monoid\ {\isacharless}\ semigroup\isanewline
-\isacommand{proof}\ intro{\isacharunderscore}classes\isanewline
+\isacommand{proof}\isanewline
 \ \ \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline
 \ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline
 \isacommand{qed}\isanewline
 \isanewline
 \isacommand{instance}\ group\ {\isacharless}\ monoid\isanewline
-\isacommand{proof}\ intro{\isacharunderscore}classes\isanewline
+\isacommand{proof}\isanewline
 \ \ \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline
 \ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
@@ -183,12 +183,12 @@
 \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
- of any classes defined in the current theory; the effect is to reduce
- to the initial statement to a number of goals that directly
- correspond to any class axioms encountered on the path upwards
- through the class hierarchy.%
+ \cite{isabelle-isar-ref}).  The initial proof step causes
+ back-chaining of class membership statements wrt.\ the hierarchy of
+ any classes defined in the current theory; the effect is to reduce to
+ the initial statement to a number of goals that directly correspond
+ to any class axioms encountered on the path upwards through the class
+ hierarchy.%
 \end{isamarkuptext}%
 %
 \isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}}

--- a/doc-src/AxClass/generated/Product.tex	Mon Oct 23 22:10:36 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex	Mon Oct 23 22:11:24 2000 +0200
@@ -40,8 +40,7 @@
  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 $\INSTANCE$ with the trivial proof
- $\BY{intro_classes}$.
+ required by means of an $\INSTANCE$ with the default proof $\DDOT$.
 
  \medskip Thus, we may observe the following discipline of using
  syntactic classes.  Overloaded polymorphic constants have their type
@@ -52,8 +51,7 @@
  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{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\ \isacommand{{\isachardot}{\isachardot}}\isanewline
 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
 \ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}%
 \begin{isamarkuptext}%