# HG changeset patch
# User nipkow
# Date 1194524599 -3600
# Node ID ef2a8a3bae4a7547ebf89df2b668b4cfecf45a87
# Parent  6eb185959aec8bf3d1a6576762d7cec0a38d5994
tuned

diff -r 6eb185959aec -r ef2a8a3bae4a doc-src/TutorialI/Fun/document/fun0.tex
--- 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.
 
diff -r 6eb185959aec -r ef2a8a3bae4a doc-src/TutorialI/Fun/fun0.thy
--- a/doc-src/TutorialI/Fun/fun0.thy	Thu Nov 08 13:23:04 2007 +0100
+++ b/doc-src/TutorialI/Fun/fun0.thy	Thu Nov 08 13:23:19 2007 +0100
@@ -79,12 +79,8 @@
 Isabelle's automatic termination prover for \isacommand{fun} has a
 fixed notion of the \emph{size} (of type @{typ 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 @{text t} comes
-with its own size function (named @{text"t.size"}) which counts the
-number of constructors in a term of type @{text t} --- more precisely
-those constructors where one of the arguments is of the type itself:
-@{const Suc} in the case of @{typ nat} and @{const "op #"} 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.