author paulson Thu, 16 Nov 2000 10:47:11 +0100 changeset 10475 77fafa07fc8f parent 10474 25caae39bd7a child 10476 dbc181a32702
ground terms section: new intro
--- 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}