--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Fri May 18 16:45:55 2001 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Fri May 18 17:18:43 2001 +0200
@@ -33,7 +33,7 @@
Isabelle because the termination proof is not as obvious since
\isa{map{\isacharunderscore}bt} is only partially applied.
-The following lemma has a canonical proof:%
+The following lemma has a simple proof by induction:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline