doc-src/TutorialI/Recdef/examples.thy
changeset 8771 026f37a86ea7
parent 8745 13b32661dde4
child 9541 d17c0b34d5c8
     1.1 --- a/doc-src/TutorialI/Recdef/examples.thy	Sun Apr 23 11:41:45 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/examples.thy	Tue Apr 25 08:09:10 2000 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  text{*\noindent
     1.6  The definition of \isa{fib} is accompanied by a \bfindex{measure function}
     1.7 -\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a
     1.8 +\isa{\isasymlambda{}n.$\;$n} which maps the argument of \isa{fib} to a
     1.9  natural number. The requirement is that in each equation the measure of the
    1.10  argument on the left-hand side is strictly greater than the measure of the
    1.11  argument of each recursive call. In the case of \isa{fib} this is
    1.12 @@ -83,7 +83,7 @@
    1.13    "swap12 zs       = zs";
    1.14  
    1.15  text{*\noindent
    1.16 -In the non-recursive case the termination measure degenerates to the empty
    1.17 +For non-recursive functions the termination measure degenerates to the empty
    1.18  set \isa{\{\}}.
    1.19  *}
    1.20