--- a/src/HOL/Induct/Term.thy Tue Oct 16 17:56:12 2001 +0200
+++ b/src/HOL/Induct/Term.thy Tue Oct 16 17:58:13 2001 +0200
@@ -36,7 +36,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))"
- apply (induct t and ts rule: term.induct)
+ apply (induct t and ts)
apply simp_all
done
@@ -50,7 +50,7 @@
proof -
case rule_context
have "P t \<and> list_all P ts"
- apply (induct t and ts rule: term.induct)
+ apply (induct t and ts)
apply (rule rule_context)
apply (rule rule_context)
apply assumption