1.1 --- a/doc-src/TutorialI/Recdef/Nested1.thy	Mon Oct 09 09:33:45 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/Nested1.thy	Mon Oct 09 10:18:21 2000 +0200
     1.3 @@ -4,12 +4,12 @@
     1.4  consts trev  :: "('a,'b)term \<Rightarrow> ('a,'b)term";
     1.5  
     1.6  text{*\noindent
     1.7 -Although the definition of @{term"trev"} is quite natural, we will have
     1.8 +Although the definition of @{term trev} is quite natural, we will have
     1.9  overcome a minor difficulty in convincing Isabelle of is termination.
    1.10  It is precisely this difficulty that is the \textit{raison d'\^etre} of
    1.11  this subsection.
    1.12  
    1.13 -Defining @{term"trev"} by \isacommand{recdef} rather than \isacommand{primrec}
    1.14 +Defining @{term trev} by \isacommand{recdef} rather than \isacommand{primrec}
    1.15  simplifies matters because we are now free to use the recursion equation
    1.16  suggested at the end of \S\ref{sec:nested-datatype}:
    1.17  *};
    1.18 @@ -19,22 +19,22 @@
    1.19   "trev (App f ts) = App f (rev(map trev ts))";
    1.20  
    1.21  text{*\noindent
    1.22 -Remember that function @{term"size"} is defined for each \isacommand{datatype}.
    1.23 +Remember that function @{term size} is defined for each \isacommand{datatype}.
    1.24  However, the definition does not succeed. Isabelle complains about an
    1.25  unproved termination condition
    1.26  @{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
    1.27 -where @{term"set"} returns the set of elements of a list
    1.28 +where @{term set} returns the set of elements of a list
    1.29  and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
    1.30  function automatically defined by Isabelle
    1.31 -(when @{text"term"} was defined).  First we have to understand why the
    1.32 -recursive call of @{term"trev"} underneath @{term"map"} leads to the above
    1.33 -condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"}
    1.34 -will apply @{term"trev"} only to elements of @{term"ts"}. Thus the above
    1.35 -condition expresses that the size of the argument @{term"t : set ts"} of any
    1.36 -recursive call of @{term"trev"} is strictly less than @{term"size(App f ts) =
    1.37 +(when @{text term} was defined).  First we have to understand why the
    1.38 +recursive call of @{term trev} underneath @{term map} leads to the above
    1.39 +condition. The reason is that \isacommand{recdef} ``knows'' that @{term map}
    1.40 +will apply @{term trev} only to elements of @{term ts}. Thus the above
    1.41 +condition expresses that the size of the argument @{prop"t : set ts"} of any
    1.42 +recursive call of @{term trev} is strictly less than @{prop"size(App f ts) =
    1.43  Suc(term_list_size ts)"}.  We will now prove the termination condition and
    1.44  continue with our definition.  Below we return to the question of how
    1.45 -\isacommand{recdef} ``knows'' about @{term"map"}.
    1.46 +\isacommand{recdef} ``knows'' about @{term map}.
    1.47  *};
    1.48  
    1.49  (*<*)