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




