1.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Fri Jan 12 16:28:14 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Fri Jan 12 16:32:01 2001 +0100
     1.3 @@ -19,8 +19,8 @@
     1.4  According to the measure function, the second argument should decrease with
     1.5  each recursive call. The resulting termination condition
     1.6  @{term[display]"n ~= 0 ==> m mod n < n"}
     1.7 -is provded automatically because it is already present as a lemma in the
     1.8 -arithmetic library. Thus the recursion equation becomes a simplification
     1.9 +is proved automatically because it is already present as a lemma in
    1.10 +HOL\@.  Thus the recursion equation becomes a simplification
    1.11  rule. Of course the equation is nonterminating if we are allowed to unfold
    1.12  the recursive call inside the @{text else} branch, which is why programming
    1.13  languages and our simplifier don't do that. Unfortunately the simplifier does