diff -r ab90e95ae02e -r b098158a3f39 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Thu Mar 17 15:12:03 2005 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Mar 18 14:31:50 2005 +0100
@@ -152,9 +152,11 @@
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
+\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
+\isanewline
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -182,9 +184,11 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
+\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
+\isanewline
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -213,17 +217,21 @@
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
+\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
+\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
+\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
+\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex