--- 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)";