doc-src/TutorialI/Ifexpr/Ifexpr.thy

--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -84,7 +84,7 @@
 *}
 
 apply(induct_tac b);
-apply(auto).;
+by(auto);
 
 text{*\noindent
 In fact, all proofs in this case study look exactly like this. Hence we do
@@ -127,11 +127,11 @@
   "\\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
 (*<*)
 apply(induct_tac b);
-apply(auto).;
+by(auto);
 
 theorem "valif (norm b) env = valif b env";
 apply(induct_tac b);
-apply(auto).;
+by(auto);
 (*>*)
 text{*\noindent
 Note that the lemma does not have a name, but is implicitly used in the proof
@@ -153,14 +153,14 @@
 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).;
+by(auto);
 
 theorem "normal(norm b)";
 apply(induct_tac b);
-apply(auto).;
+by(auto);
 
 end
 (*>*)