diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Ifexpr/Ifexpr.thy
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Tue Apr 25 08:09:10 2000 +0200
@@ -61,7 +61,7 @@
 \subsubsection{Transformation into and of If-expressions}
 
 The type \isa{boolex} is close to the customary representation of logical
-formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to
+formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
 translate from \isa{boolex} into \isa{ifex}:
 *}
 
@@ -153,7 +153,8 @@
 normality of \isa{normif}:
 *}
 
-lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";(*<*)
+lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";
+(*<*)
 apply(induct_tac b);
 apply(auto).;
 
@@ -161,4 +162,5 @@
 apply(induct_tac b);
 apply(auto).;
 
-end(*>*)
+end
+(*>*)