--- a/doc-src/AxClass/body.tex Mon May 22 16:03:43 2000 +0200
+++ b/doc-src/AxClass/body.tex Mon May 22 16:04:32 2000 +0200
@@ -44,7 +44,8 @@
object-logic that directly uses the meta type system, such as Isabelle/HOL
\cite{isabelle-HOL}. Subsequently, we present various examples that are all
formulated within HOL, except the one of \secref{sec:ex-natclass} which is in
-FOL.
+FOL. See also \url{http://isabelle.in.tum.de/library/HOL/AxClass/} and
+\url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}.
\input{generated/Semigroups}
--- a/doc-src/AxClass/generated/Group.tex Mon May 22 16:03:43 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex Mon May 22 16:04:32 2000 +0200
@@ -195,9 +195,7 @@
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}}
--- a/src/HOL/AxClasses/Tutorial/Group.thy Mon May 22 16:03:43 2000 +0200
+++ b/src/HOL/AxClasses/Tutorial/Group.thy Mon May 22 16:04:32 2000 +0200
@@ -92,7 +92,7 @@
qed;
-subsection {* Concrete instantiation \label{sec:inst-arity} *};
+subsection {* Concrete instantiation *};
defs
times_bool_def: "x [*] y == x ~= (y::bool)"