--- a/doc-src/TutorialI/Fun/document/fun0.tex Thu Nov 08 13:23:04 2007 +0100
+++ b/doc-src/TutorialI/Fun/document/fun0.tex Thu Nov 08 13:23:19 2007 +0100
@@ -95,12 +95,8 @@
Isabelle's automatic termination prover for \isacommand{fun} has a
fixed notion of the \emph{size} (of type \isa{nat}) of an
argument. The size of a natural number is the number itself. The size
-of a list is its length. In general, every datatype \isa{t} comes
-with its own size function (named \isa{t{\isachardot}size}) which counts the
-number of constructors in a term of type \isa{t} --- more precisely
-those constructors where one of the arguments is of the type itself:
-\isa{Suc} in the case of \isa{nat} and \isa{op\ {\isacharhash}} in the case
-of lists. A recursive function is accepted if \isacommand{fun} can
+of a list is its length. For the general case see \S\ref{sec:general-datatype}.
+A recursive function is accepted if \isacommand{fun} can
show that the size of one fixed argument becomes smaller with each
recursive call.