1.1 --- a/doc-src/TutorialI/Fun/fun0.thy	Thu Nov 08 13:23:04 2007 +0100
     1.2 +++ b/doc-src/TutorialI/Fun/fun0.thy	Thu Nov 08 13:23:19 2007 +0100
     1.3 @@ -79,12 +79,8 @@
     1.4  Isabelle's automatic termination prover for \isacommand{fun} has a
     1.5  fixed notion of the \emph{size} (of type @{typ nat}) of an
     1.6  argument. The size of a natural number is the number itself. The size
     1.7 -of a list is its length. In general, every datatype @{text t} comes
     1.8 -with its own size function (named @{text"t.size"}) which counts the
     1.9 -number of constructors in a term of type @{text t} --- more precisely
    1.10 -those constructors where one of the arguments is of the type itself:
    1.11 -@{const Suc} in the case of @{typ nat} and @{const "op #"} in the case
    1.12 -of lists. A recursive function is accepted if \isacommand{fun} can
    1.13 +of a list is its length. For the general case see \S\ref{sec:general-datatype}.
    1.14 +A recursive function is accepted if \isacommand{fun} can
    1.15  show that the size of one fixed argument becomes smaller with each
    1.16  recursive call.
    1.17