diff -r 25caae39bd7a -r 77fafa07fc8f doc-src/TutorialI/Inductive/Advanced.tex
--- a/doc-src/TutorialI/Inductive/Advanced.tex	Thu Nov 16 10:44:59 2000 +0100
+++ b/doc-src/TutorialI/Inductive/Advanced.tex	Thu Nov 16 10:47:11 2000 +0100
@@ -1,17 +1,17 @@
 
-The next examples illustrate advanced features of inductive  definitions. 
+This section describes advanced features of inductive definitions. 
 The premises of introduction rules may contain universal quantifiers and
 monotonic functions.  Theorems may be proved by rule inversion.
 
 \subsection{Universal quantifiers in introduction rules}
 \label{sec:gterm-datatype}
 
-A \textbf{ground} term is a term constructed from constant and function 
-symbols alone: no variables. To simplify matters further, 
-we regard a constant as a function applied to the null argument 
-list. Let us declare a datatype \isa{gterm} for the type of ground 
-terms. It is a type constructor whose argument is a type of 
-function symbols. 
+As a running example, this section develops the theory of \textbf{ground
+terms}: terms constructed from constant and function 
+symbols but not variables. To simplify matters further, we regard a
+constant as a function applied to the null argument  list.  Let us declare a
+datatype \isa{gterm} for the type of ground  terms. It is a type constructor
+whose argument is a type of  function symbols. 
 \begin{isabelle}
 \isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list"
 \end{isabelle}