--- a/doc-src/TutorialI/Datatype/Nested.thy Sun Jun 22 23:08:32 2008 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Mon Jun 23 15:26:47 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 rule: term.induct, simp_all);
+apply(induct_tac t and ts, 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 rule: term.induct)
+apply (induct_tac t and ts)
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 rule: term.induct, simp_all)
+apply (induct_tac t and ts, simp_all)
done
(*>*)