1.1 --- a/doc-src/TutorialI/Datatype/ABexpr.thy	Sun Jun 22 23:08:32 2008 +0200
     1.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Mon Jun 23 15:26:47 2008 +0200
     1.3 @@ -93,10 +93,9 @@
     1.4  
     1.5  lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
     1.6          evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
     1.7 -apply(induct_tac a and b rule: aexp_bexp.induct);
     1.8 +apply(induct_tac a and b);
     1.9  
    1.10 -txt{*\noindent Unfortunately, induction needs to be told explicitly which induction rule to use (via @{text"rule:"}).
    1.11 -The resulting 8 goals (one for each constructor) are proved in one fell swoop:
    1.12 +txt{*\noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop:
    1.13  *}
    1.14  
    1.15  apply simp_all;
    1.16 @@ -108,7 +107,7 @@
    1.17  \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
    1.18  where each variable $x@i$ is of type $\tau@i$. Induction is started by
    1.19  \begin{isabelle}
    1.20 -\isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$ @{text"rule:"} $\tau@1$@{text"_"}\dots@{text"_"}$\tau@n$@{text".induct)"}
    1.21 +\isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text ")"}
    1.22  \end{isabelle}
    1.23  
    1.24  \begin{exercise}
    1.25 @@ -138,7 +137,7 @@
    1.26  
    1.27  lemma " evala (norma a) env = evala a env 
    1.28        \<and> (\<forall> t e. evala (normb b t e) env = evala (IF b t e) env)"
    1.29 -apply (induct_tac a and b rule: aexp_bexp.induct)
    1.30 +apply (induct_tac a and b)
    1.31  apply (simp_all)
    1.32  done
    1.33  
    1.34 @@ -156,7 +155,7 @@
    1.35  
    1.36  lemma "normala (norma (a::'a aexp)) \<and>
    1.37         (\<forall> (t::'a aexp) e. (normala t \<and> normala e) \<longrightarrow> normala (normb b t e))"
    1.38 -apply (induct_tac a and b rule: aexp_bexp.induct)
    1.39 +apply (induct_tac a and b)
    1.40  apply (auto)
    1.41  done
    1.42