# HG changeset patch
# User nipkow
# Date 1213273207 -7200
# Node ID 968a1450ae3577edfc882a1531121be3de74e337
# Parent  e1c49eb8cee691745d7a27580a97cf5154d7d35a
had to add rule: because induct_tac no longer works correctly

diff -r e1c49eb8cee6 -r 968a1450ae35 doc-src/TutorialI/Datatype/ABexpr.thy
--- a/doc-src/TutorialI/Datatype/ABexpr.thy	Thu Jun 12 14:10:41 2008 +0200
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Thu Jun 12 14:20:07 2008 +0200
@@ -95,7 +95,7 @@
         evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
 apply(induct_tac a and b rule: aexp_bexp.induct);
 
-txt{*\noindent
+txt{*\noindent Unfortunately, induction needs to be told explicitly which induction rule to use (via @{text"rule:"}).
 The resulting 8 goals (one for each constructor) are proved in one fell swoop:
 *}
 
@@ -108,7 +108,7 @@
 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
 where each variable $x@i$ is of type $\tau@i$. Induction is started by
 \begin{isabelle}
-\isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text")"}
+\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)"}
 \end{isabelle}
 
 \begin{exercise}
diff -r e1c49eb8cee6 -r 968a1450ae35 doc-src/TutorialI/Datatype/document/ABexpr.tex
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Thu Jun 12 14:10:41 2008 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Thu Jun 12 14:20:07 2008 +0200
@@ -119,7 +119,7 @@
 \isacommand{apply}\isamarkupfalse%
 {\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b\ rule{\isacharcolon}\ aexp{\isacharunderscore}bexp{\isachardot}induct{\isacharparenright}%
 \begin{isamarkuptxt}%
-\noindent
+\noindent Unfortunately, induction needs to be told explicitly which induction rule to use (via \isa{rule{\isacharcolon}}).
 The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
@@ -138,7 +138,7 @@
 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
 where each variable $x@i$ is of type $\tau@i$. Induction is started by
 \begin{isabelle}
-\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$\isa{{\isacharparenright}}
+\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$ \isa{rule{\isacharcolon}} $\tau@1$\isa{{\isacharunderscore}}\dots\isa{{\isacharunderscore}}$\tau@n$\isa{{\isachardot}induct{\isacharparenright}}
 \end{isabelle}
 
 \begin{exercise}