--- a/doc-src/TutorialI/Misc/document/Itrev.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Tue Dec 17 11:05:41 2002 +0100
@@ -91,6 +91,7 @@
just not true. The correct generalization is%
\end{isamarkuptxt}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
@@ -118,6 +119,7 @@
for all \isa{ys} instead of a fixed one:%
\end{isamarkuptxt}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
@@ -157,6 +159,7 @@
\index{induction heuristics|)}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables: