diff -r c50fc8023ac0 -r a7f961fb62c6 doc-src/AxClass/Group/Group.thy
--- a/doc-src/AxClass/Group/Group.thy	Mon Oct 23 22:09:52 2000 +0200
+++ b/doc-src/AxClass/Group/Group.thy	Mon Oct 23 22:10:36 2000 +0200
@@ -182,14 +182,14 @@
 *}
 
 instance monoid < semigroup
-proof intro_classes
+proof
   fix x y z :: "'a\<Colon>monoid"
   show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
     by (rule monoid.assoc)
 qed
 
 instance group < monoid
-proof intro_classes
+proof
   fix x y z :: "'a\<Colon>group"
   show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
     by (rule semigroup.assoc)
@@ -203,12 +203,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 @{text intro_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.
 *}