--- a/doc-src/TutorialI/Recdef/document/simplification.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Fri Jan 12 16:07:20 2001 +0100
@@ -20,8 +20,8 @@
\begin{isabelle}%
\ \ \ \ \ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
\end{isabelle}
-is provded automatically because it is already present as a lemma in the
-arithmetic library. Thus the recursion equation becomes a simplification
+is proved automatically because it is already present as a lemma in
+HOL\@. Thus the recursion equation becomes a simplification
rule. Of course the equation is nonterminating if we are allowed to unfold
the recursive call inside the \isa{else} branch, which is why programming
languages and our simplifier don't do that. Unfortunately the simplifier does