# HG changeset patch
# User wenzelm
# Date 959004272 -7200
# Node ID 490637ba1d7ff04aff24b12b094dd502572e400a
# Parent  7c04c98132c4f4082b0b350b2fe4388952b99cba
tuned;

diff -r 7c04c98132c4 -r 490637ba1d7f doc-src/AxClass/body.tex
--- 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}
 
diff -r 7c04c98132c4 -r 490637ba1d7f doc-src/AxClass/generated/Group.tex
--- 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}}
diff -r 7c04c98132c4 -r 490637ba1d7f src/HOL/AxClasses/Tutorial/Group.thy
--- 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)"