1.1 --- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Nov 12 10:44:55 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Nov 12 10:56:38 2001 +0100
     1.3 @@ -112,10 +112,12 @@
     1.4  \isacommand{lemma}\ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
     1.5  \ \ \ \ \ {\isachardoublequote}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequote}\isanewline
     1.6  \isamarkupfalse%
     1.7 -\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isanewline
     1.8 -\isanewline
     1.9 -\isanewline
    1.10 -\isamarkupfalse%
    1.11 +\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isamarkupfalse%
    1.12 +%
    1.13 +\begin{isamarkuptext}%
    1.14 +the following declaration isn't actually used%
    1.15 +\end{isamarkuptext}%
    1.16 +\isamarkuptrue%
    1.17  \isacommand{consts}\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    1.18  \isamarkupfalse%
    1.19  \isacommand{primrec}\isanewline