--- a/doc-src/TutorialI/Misc/document/Itrev.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed Jan 15 16:43:12 2003 +0100
@@ -91,9 +91,9 @@
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%
+\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptxt}%
@@ -119,9 +119,9 @@
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%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -159,7 +159,6 @@
\index{induction heuristics|)}%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables: