--- a/doc-src/TutorialI/Inductive/document/Advanced.tex Thu Mar 17 15:12:03 2005 +0100
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Fri Mar 18 14:31:50 2005 +0100
@@ -59,7 +59,6 @@
\isamarkupfalse%
\isamarkupfalse%
\isanewline
-\isanewline
\isamarkupfalse%
\isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}\isamarkupfalse%
%
@@ -134,7 +133,6 @@
\isanewline
\isanewline
\isanewline
-\isanewline
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
\isamarkupfalse%
@@ -196,7 +194,6 @@
\isamarkupfalse%
\isamarkupfalse%
\isanewline
-\isanewline
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
\isamarkupfalse%
@@ -205,7 +202,6 @@
\isamarkupfalse%
\isanewline
\isanewline
-\isanewline
\isamarkupfalse%
\isacommand{end}\isanewline
\isanewline