# HG changeset patch
# User haftmann
# Date 1213168132 -7200
# Node ID ef2634bef947b0a1074587647247fdd32c3c227d
# Parent  574a09bcdb0295f6c8235747f3a5f65d92ab2fa1
explicit rule for induct_tac

diff -r 574a09bcdb02 -r ef2634bef947 doc-src/TutorialI/Datatype/ABexpr.thy
--- 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
 
diff -r 574a09bcdb02 -r ef2634bef947 doc-src/TutorialI/Datatype/Nested.thy
--- 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
 (*>*)
 
diff -r 574a09bcdb02 -r ef2634bef947 doc-src/TutorialI/Datatype/document/ABexpr.tex
--- 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:%
diff -r 574a09bcdb02 -r ef2634bef947 doc-src/TutorialI/Datatype/document/Nested.tex
--- 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