--- a/doc-src/TutorialI/Recdef/document/Induction.tex Sun Apr 23 11:41:45 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Apr 25 08:09:10 2000 +0200
@@ -13,7 +13,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%
\end{isamarkuptext}%
\isacommand{lemma}~{"}map~f~(sep(x,xs))~=~sep(f~x,~map~f~xs){"}%
\begin{isamarkuptxt}%