doc-src/TutorialI/Overview/RECDEF.thy

--- a/doc-src/TutorialI/Overview/RECDEF.thy	Wed Jun 26 10:26:46 2002 +0200
+++ b/doc-src/TutorialI/Overview/RECDEF.thy	Wed Jun 26 11:07:14 2002 +0200
@@ -61,8 +61,14 @@
 
 subsubsection{*Induction*}
 
+text{*
+Every recursive definition provides an induction theorem, for example
+@{thm[source]sep.induct}:
+@{thm[display,margin=70] sep.induct[no_vars]}
+*}
+(*<*)thm sep.induct[no_vars](*>*)
+
 lemma "map f (sep(x,xs)) = sep(f x, map f xs)"
-thm sep.induct
 apply(induct_tac x xs rule: sep.induct)
 apply simp_all
 done