1.1 --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Fri Jul 28 13:04:59 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Fri Jul 28 16:02:51 2000 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4  *}
     1.5  
     1.6  apply(induct_tac b);
     1.7 -apply(auto).;
     1.8 +by(auto);
     1.9  
    1.10  text{*\noindent
    1.11  In fact, all proofs in this case study look exactly like this. Hence we do
    1.12 @@ -127,11 +127,11 @@
    1.13    "\\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
    1.14  (*<*)
    1.15  apply(induct_tac b);
    1.16 -apply(auto).;
    1.17 +by(auto);
    1.18  
    1.19  theorem "valif (norm b) env = valif b env";
    1.20  apply(induct_tac b);
    1.21 -apply(auto).;
    1.22 +by(auto);
    1.23  (*>*)
    1.24  text{*\noindent
    1.25  Note that the lemma does not have a name, but is implicitly used in the proof
    1.26 @@ -153,14 +153,14 @@
    1.27  normality of \isa{normif}:
    1.28  *}
    1.29  
    1.30 -lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";
    1.31 +lemma[simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";
    1.32  (*<*)
    1.33  apply(induct_tac b);
    1.34 -apply(auto).;
    1.35 +by(auto);
    1.36  
    1.37  theorem "normal(norm b)";
    1.38  apply(induct_tac b);
    1.39 -apply(auto).;
    1.40 +by(auto);
    1.41  
    1.42  end
    1.43  (*>*)