--- 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
+(*>*)