doc-src/TutorialI/Ifexpr/Ifexpr.thy

 txt{*\noindent
 The proof is canonical:
 *}
 
 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
 not show them below.
 

 
 lemma [simp]:
   "\\<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
 of the theorem shown above because of the \isa{[simp]} attribute.
 

 text{*\noindent
 and prove \isa{normal(norm b)}. Of course, this requires a lemma about
 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
 (*>*)