diff -r bfab4d4b7516 -r 026f37a86ea7 doc-src/TutorialI/Recdef/Induction.thy --- a/doc-src/TutorialI/Recdef/Induction.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Recdef/Induction.thy Tue Apr 25 08:09:10 2000 +0200 @@ -15,7 +15,7 @@ \textbf{recursion induction}. Roughly speaking, it requires you to prove for each \isacommand{recdef} equation that the property you are trying to establish holds for the left-hand side provided it holds -for all recursive calls on the right-hand side. Here is a simple example: +for all recursive calls on the right-hand side. Here is a simple example *} lemma "map f (sep(x,xs)) = sep(f x, map f xs)";