| changeset 11293 | 6878bb02a7f9 |
| parent 11236 | 17403c5a9eb1 |
| child 12815 | 1f073030b97a |
--- a/doc-src/TutorialI/Overview/RECDEF.thy Thu May 10 09:41:45 2001 +0200 +++ b/doc-src/TutorialI/Overview/RECDEF.thy Thu May 10 09:48:50 2001 +0200 @@ -48,6 +48,7 @@ subsubsection{*Induction*} 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