--- a/doc-src/TutorialI/Recdef/examples.thy Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Recdef/examples.thy Fri Sep 01 19:09:44 2000 +0200
@@ -13,13 +13,13 @@
"fib (Suc(Suc x)) = fib x + fib (Suc x)";
text{*\noindent
-The definition of \isa{fib} is accompanied by a \bfindex{measure function}
-@{term"%n. n"} which maps the argument of \isa{fib} to a
+The definition of @{term"fib"} is accompanied by a \bfindex{measure function}
+@{term"%n. n"} which maps the argument of @{term"fib"} to a
natural number. The requirement is that in each equation the measure of the
argument on the left-hand side is strictly greater than the measure of the
-argument of each recursive call. In the case of \isa{fib} this is
+argument of each recursive call. In the case of @{term"fib"} this is
obviously true because the measure function is the identity and
-@{term"Suc(Suc x)"} is strictly greater than both \isa{x} and
+@{term"Suc(Suc x)"} is strictly greater than both @{term"x"} and
@{term"Suc x"}.
Slightly more interesting is the insertion of a fixed element
@@ -55,8 +55,8 @@
"sep1(a, xs) = xs";
text{*\noindent
-This defines exactly the same function as \isa{sep} above, i.e.\
-\isa{sep1 = sep}.
+This defines exactly the same function as @{term"sep"} above, i.e.\
+@{prop"sep1 = sep"}.
\begin{warn}
\isacommand{recdef} only takes the first argument of a (curried)
@@ -84,7 +84,7 @@
text{*\noindent
For non-recursive functions the termination measure degenerates to the empty
-set \isa{\{\}}.
+set @{term"{}"}.
*}
(*<*)