doc-src/TutorialI/Datatype/Nested.thy

 (*<*)
 theory Nested = ABexpr:
 (*>*)
 
 text{*
+\index{datatypes!and nested recursion}%
 So far, all datatypes had the property that on the right-hand side of their
-definition they occurred only at the top-level, i.e.\ directly below a
+definition they occurred only at the top-level: directly below a
 constructor. Now we consider \emph{nested recursion}, where the recursive
 datatype occurs nested in some other datatype (but not inside itself!).
 Consider the following model of terms
 where function symbols can be applied to a list of arguments:
 *}

 
   "substs s [] = []"
   "substs s (t # ts) = subst s t # substs s ts";
 
 text{*\noindent
-Individual equations in a primrec definition may be named as shown for @{thm[source]subst_App}.
+Individual equations in a \commdx{primrec} definition may be
+named as shown for @{thm[source]subst_App}.
 The significance of this device will become apparent below.
 
 Similarly, when proving a statement about terms inductively, we need
 to prove a related statement about term lists simultaneously. For example,
 the fact that the identity substitution does not change a term needs to be