# HG changeset patch
# User nipkow
# Date 1063620994 -7200
# Node ID f471cd4c7282c5334d31f8537aeb94cb8f5f50ce
# Parent  26dfcd0ac436744cbe4207d845faf8556932f203
*** empty log message ***

diff -r 26dfcd0ac436 -r f471cd4c7282 doc-src/TutorialI/Datatype/Fundata.thy
--- 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.
diff -r 26dfcd0ac436 -r f471cd4c7282 doc-src/TutorialI/Datatype/document/Fundata.tex
--- 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.