doc-src/TutorialI/Recdef/examples.thy
changeset 9792 bbefb6ce5cb2
parent 9541 d17c0b34d5c8
child 9933 9feb1e0c4cb3
     1.1 --- a/doc-src/TutorialI/Recdef/examples.thy	Fri Sep 01 18:29:52 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/examples.thy	Fri Sep 01 19:09:44 2000 +0200
     1.3 @@ -13,13 +13,13 @@
     1.4    "fib (Suc(Suc x)) = fib x + fib (Suc x)";
     1.5  
     1.6  text{*\noindent
     1.7 -The definition of \isa{fib} is accompanied by a \bfindex{measure function}
     1.8 -@{term"%n. n"} which maps the argument of \isa{fib} to a
     1.9 +The definition of @{term"fib"} is accompanied by a \bfindex{measure function}
    1.10 +@{term"%n. n"} which maps the argument of @{term"fib"} to a
    1.11  natural number. The requirement is that in each equation the measure of the
    1.12  argument on the left-hand side is strictly greater than the measure of the
    1.13 -argument of each recursive call. In the case of \isa{fib} this is
    1.14 +argument of each recursive call. In the case of @{term"fib"} this is
    1.15  obviously true because the measure function is the identity and
    1.16 -@{term"Suc(Suc x)"} is strictly greater than both \isa{x} and
    1.17 +@{term"Suc(Suc x)"} is strictly greater than both @{term"x"} and
    1.18  @{term"Suc x"}.
    1.19  
    1.20  Slightly more interesting is the insertion of a fixed element
    1.21 @@ -55,8 +55,8 @@
    1.22    "sep1(a, xs)     = xs";
    1.23  
    1.24  text{*\noindent
    1.25 -This defines exactly the same function as \isa{sep} above, i.e.\
    1.26 -\isa{sep1 = sep}.
    1.27 +This defines exactly the same function as @{term"sep"} above, i.e.\
    1.28 +@{prop"sep1 = sep"}.
    1.29  
    1.30  \begin{warn}
    1.31    \isacommand{recdef} only takes the first argument of a (curried)
    1.32 @@ -84,7 +84,7 @@
    1.33  
    1.34  text{*\noindent
    1.35  For non-recursive functions the termination measure degenerates to the empty
    1.36 -set \isa{\{\}}.
    1.37 +set @{term"{}"}.
    1.38  *}
    1.39  
    1.40  (*<*)