summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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