doc-src/TutorialI/Recdef/examples.thy

   "fib 0 = 0"
   "fib 1 = 1"
   "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
 between any two elements of a list:
 *}

 recdef sep1 "measure (\\<lambda>(a,xs). length xs)"
   "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
   "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)
   recursive function into account. This means both the termination measure
   and pattern matching can only use that first argument. In general, you will

   "swap12 (x#y#zs) = y#x#zs"
   "swap12 zs       = zs";
 
 text{*\noindent
 For non-recursive functions the termination measure degenerates to the empty
-set \isa{\{\}}.
+set @{term"{}"}.
 *}
 
 (*<*)
 end
 (*>*)