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  (*<*)