--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Mon Aug 28 15:13:55 2000 +0200
@@ -37,7 +37,7 @@
The following lemma has a canonical proof%
\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{by}{\isacharparenleft}induct{\isacharunderscore}tac\ {\isachardoublequote}T{\isachardoublequote}{\isacharcomma}\ auto{\isacharparenright}%
+\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ {\isachardoublequote}T{\isachardoublequote}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
but it is worth taking a look at the proof state after the induction step