1.1 --- a/doc-src/TutorialI/Datatype/ABexpr.thy	Thu Jun 12 14:10:41 2008 +0200
     1.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Thu Jun 12 14:20:07 2008 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4          evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
     1.5  apply(induct_tac a and b rule: aexp_bexp.induct);
     1.6  
     1.7 -txt{*\noindent
     1.8 +txt{*\noindent Unfortunately, induction needs to be told explicitly which induction rule to use (via @{text"rule:"}).
     1.9  The resulting 8 goals (one for each constructor) are proved in one fell swoop:
    1.10  *}
    1.11  
    1.12 @@ -108,7 +108,7 @@
    1.13  \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
    1.14  where each variable $x@i$ is of type $\tau@i$. Induction is started by
    1.15  \begin{isabelle}
    1.16 -\isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text")"}
    1.17 +\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.18  \end{isabelle}
    1.19  
    1.20  \begin{exercise}