diff -r a7f961fb62c6 -r d78de58fe368 doc-src/AxClass/generated/Group.tex
--- 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}}