--- a/doc-src/TutorialI/Datatype/Fundata.thy Sun Sep 14 17:53:27 2003 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy Mon Sep 15 12:16:34 2003 +0200
@@ -25,9 +25,9 @@
"map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))"
text{*\noindent This is a valid \isacommand{primrec} definition because the
-recursive calls of @{term"map_bt"} involve only subtrees obtained from
-@{term"F"}: the left-hand side. Thus termination is assured. The
-seasoned functional programmer might try expressing
+recursive calls of @{term"map_bt"} involve only subtrees of
+@{term"F"}, which is itself a subterm of the left-hand side. Thus termination
+is assured. The seasoned functional programmer might try expressing
@{term"%i. map_bt f (F i)"} as @{term"map_bt f o F"}, which Isabelle
however will reject. Applying @{term"map_bt"} to only one of its arguments
makes the termination proof less obvious.
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Sun Sep 14 17:53:27 2003 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Mon Sep 15 12:16:34 2003 +0200
@@ -31,9 +31,9 @@
%
\begin{isamarkuptext}%
\noindent This is a valid \isacommand{primrec} definition because the
-recursive calls of \isa{map{\isacharunderscore}bt} involve only subtrees obtained from
-\isa{F}: the left-hand side. Thus termination is assured. The
-seasoned functional programmer might try expressing
+recursive calls of \isa{map{\isacharunderscore}bt} involve only subtrees of
+\isa{F}, which is itself a subterm of the left-hand side. Thus termination
+is assured. The seasoned functional programmer might try expressing
\isa{{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}} as \isa{map{\isacharunderscore}bt\ f\ {\isasymcirc}\ F}, which Isabelle
however will reject. Applying \isa{map{\isacharunderscore}bt} to only one of its arguments
makes the termination proof less obvious.