1.1 --- a/doc-src/IsarRef/generic.tex	Wed Jan 09 08:33:01 2008 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Wed Jan 09 08:57:12 2008 +0100
     1.3 @@ -519,7 +519,7 @@
     1.4  the full generality of locales combined with the commodity of type classes
     1.5  (notably type-inference).  See \cite{isabelle-classes} for a short tutorial.
     1.6  
     1.7 -\indexisarcmd{instance}\indexisarcmd{class}\indexisarcmd{print-classes}
     1.8 +\indexisarcmd{class}\indexisarcmd{instantiation}\indexisarcmd{subclass}\indexisarcmd{class}\indexisarcmd{print-classes}
     1.9  \begin{matharray}{rcl}
    1.10    \isarcmd{class} & : & \isartrans{theory}{local{\dsh}theory} \\
    1.11    \isarcmd{instantiation} & : & \isartrans{theory}{local{\dsh}theory} \\

     2.1 --- a/doc-src/IsarRef/logics.tex	Wed Jan 09 08:33:01 2008 +0100
     2.2 +++ b/doc-src/IsarRef/logics.tex	Wed Jan 09 08:57:12 2008 +0100
     2.3 @@ -435,21 +435,21 @@
     2.4  
     2.5  \subsection{Recursive functions}\label{sec:recursion}
     2.6  
     2.7 -\indexisarcmdof{HOL}{primrec}
     2.8 +\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{fun}\indexisarcmdof{HOL}{function}\indexisarcmdof{HOL}{termination}
     2.9  
    2.10  \begin{matharray}{rcl}
    2.11 -  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
    2.12 -  \isarcmd{fun} & : & \isartrans{theory}{theory} \\
    2.13 -  \isarcmd{function} & : & \isartrans{theory}{proof(prove)} \\
    2.14 -  \isarcmd{termination} & : & \isartrans{theory}{proof(prove)} \\
    2.15 +  \isarcmd{primrec} & : & \isarkeep{local{\dsh}theory} \\
    2.16 +  \isarcmd{fun} & : & \isarkeep{local{\dsh}theory} \\
    2.17 +  \isarcmd{function} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
    2.18 +  \isarcmd{termination} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
    2.19  \end{matharray}
    2.20  
    2.21  \railalias{funopts}{function\_opts}
    2.22  
    2.23  \begin{rail}
    2.24 -  'primrec' parname? (equation +)
    2.25 +  'primrec' target? fixes 'where' equations
    2.26    ;
    2.27 -  equation: thmdecl? prop
    2.28 +  equations: (thmdecl? prop + '|')
    2.29    ;
    2.30    ('fun' | 'function') (funopts)? fixes 'where' clauses
    2.31    ;
    2.32 @@ -462,10 +462,10 @@
    2.33  \end{rail}
    2.34  
    2.35  \begin{descr}
    2.36 -  
    2.37 +
    2.38  \item [$\isarkeyword{primrec}$] defines primitive recursive functions over
    2.39    datatypes, see also \cite{isabelle-HOL}.
    2.40 -  
    2.41 +
    2.42  \item [$\isarkeyword{function}$] defines functions by general
    2.43    wellfounded recursion. A detailed description with examples can be
    2.44    found in \cite{isabelle-function}. The function is specified by a
    2.45 @@ -718,10 +718,10 @@
    2.46  
    2.47  \indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{inductive-set}\indexisarcmdof{HOL}{coinductive}\indexisarcmdof{HOL}{coinductive-set}\indexisarattof{HOL}{mono}
    2.48  \begin{matharray}{rcl}
    2.49 -  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
    2.50 -  \isarcmd{inductive_set} & : & \isartrans{theory}{theory} \\
    2.51 -  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
    2.52 -  \isarcmd{coinductive_set} & : & \isartrans{theory}{theory} \\
    2.53 +  \isarcmd{inductive} & : & \isarkeep{local{\dsh}theory} \\
    2.54 +  \isarcmd{inductive_set} & : & \isarkeep{local{\dsh}theory} \\
    2.55 +  \isarcmd{coinductive} & : & \isarkeep{local{\dsh}theory} \\
    2.56 +  \isarcmd{coinductive_set} & : & \isarkeep{local{\dsh}theory} \\
    2.57    mono & : & \isaratt \\
    2.58  \end{matharray}
    2.59