explicit rule for induct_tac

--- a/doc-src/TutorialI/Datatype/ABexpr.thy	Tue Jun 10 23:49:55 2008 +0200
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Wed Jun 11 09:08:52 2008 +0200
@@ -93,7 +93,7 @@
 
 lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
         evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
-apply(induct_tac a and b);
+apply(induct_tac a and b rule: aexp_bexp.induct);
 
 txt{*\noindent
 The resulting 8 goals (one for each constructor) are proved in one fell swoop:
@@ -138,7 +138,7 @@
 
 lemma " evala (norma a) env = evala a env 
       \<and> (\<forall> t e. evala (normb b t e) env = evala (IF b t e) env)"
-apply (induct_tac a and b)
+apply (induct_tac a and b rule: aexp_bexp.induct)
 apply (simp_all)
 done
 
@@ -156,7 +156,7 @@
 
 lemma "normala (norma (a::'a aexp)) \<and>
        (\<forall> (t::'a aexp) e. (normala t \<and> normala e) \<longrightarrow> normala (normb b t e))"
-apply (induct_tac a and b)
+apply (induct_tac a and b rule: aexp_bexp.induct)
 apply (auto)
 done
 

--- a/doc-src/TutorialI/Datatype/Nested.thy	Tue Jun 10 23:49:55 2008 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Wed Jun 11 09:08:52 2008 +0200
@@ -67,7 +67,7 @@
 
 lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst  Var t  = (t ::('v,'f)term)  \<and>
                   substs Var ts = (ts::('v,'f)term list)";
-apply(induct_tac t and ts, simp_all);
+apply(induct_tac t and ts rule: term.induct, simp_all);
 done
 
 text{*\noindent
@@ -105,7 +105,7 @@
 (* Exercise 1: *)
 lemma "subst  ((subst f) \<circ> g) t  = subst  f (subst g t) \<and>
        substs ((subst f) \<circ> g) ts = substs f (substs g ts)"
-apply (induct_tac t and ts)
+apply (induct_tac t and ts rule: term.induct)
 apply (simp_all)
 done
 
@@ -126,7 +126,7 @@
 
 lemma "trev (trev t) = (t::('v,'f)term) \<and> 
        trevs (trevs ts) = (ts::('v,'f)term list)"
-apply (induct_tac t and ts, simp_all)
+apply (induct_tac t and ts rule: term.induct, simp_all)
 done
 (*>*)
 

--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Tue Jun 10 23:49:55 2008 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Wed Jun 11 09:08:52 2008 +0200
@@ -117,7 +117,7 @@
 %
 \isatagproof
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b{\isacharparenright}%
+{\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b\ rule{\isacharcolon}\ aexp{\isacharunderscore}bexp{\isachardot}induct{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 The resulting 8 goals (one for each constructor) are proved in one fell swoop:%

--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Jun 10 23:49:55 2008 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Wed Jun 11 09:08:52 2008 +0200
@@ -89,7 +89,7 @@
 %
 \isatagproof
 \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
+{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts\ rule{\isacharcolon}\ term{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
 \isacommand{done}\isamarkupfalse%
 %
 \endisatagproof