1.1 --- a/doc-src/TutorialI/Datatype/Nested.thy	Tue Apr 17 15:03:41 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy	Tue Apr 17 16:54:38 2001 +0200
     1.3 @@ -5,7 +5,9 @@
     1.4  text{*
     1.5  So far, all datatypes had the property that on the right-hand side of their
     1.6  definition they occurred only at the top-level, i.e.\ directly below a
     1.7 -constructor. This is not the case any longer for the following model of terms
     1.8 +constructor. Now we consider \emph{nested recursion}, where the recursive
     1.9 +datatupe occurs nested in some other datatype (but not inside itself!).
    1.10 +Consider the following model of terms
    1.11  where function symbols can be applied to a list of arguments:
    1.12  *}
    1.13  (*<*)hide const Var(*>*)
    1.14 @@ -126,4 +128,4 @@
    1.15  *}
    1.16  (*<*)
    1.17  end
    1.18 -(*>*)
    1.19 \ No newline at end of file
    1.20 +(*>*)