# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID b6603402554862ba8315137ba5a6b9996eaf9b63
# Parent  0662f35534fe69aba8b3f0c8848a35d2d81d38fc
ported Induct to new datatypes

diff -r 0662f35534fe -r b66034025548 src/HOL/Induct/Term.thy
--- a/src/HOL/Induct/Term.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Induct/Term.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -31,7 +31,7 @@
     subst_term f1 (subst_term f2 t)"
 and "subst_term_list (subst_term f1 \<circ> f2) ts =
     subst_term_list f1 (subst_term_list f2 ts)"
-  by (induct t and ts) simp_all
+  by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
 
 
 text {* \medskip Alternative induction rule *}
@@ -41,7 +41,7 @@
     and app: "!!f ts. (\<forall>t \<in> set ts. P t) ==> P (App f ts)"
   shows term_induct2: "P t"
     and "\<forall>t \<in> set ts. P t"
-  apply (induct t and ts)
+  apply (induct t and ts rule: subst_term.induct subst_term_list.induct)
      apply (rule var)
     apply (rule app)
     apply assumption