doc-src/AxClass/generated/Group.tex

  (see also \cite{isabelle-isar-ref}).  The $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.
-
- any logical class axioms as subgoals.%
+ through the class hierarchy.%
 \end{isamarkuptext}%
 %
 \isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}}
 %
 \begin{isamarkuptext}%