tuned

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

--- a/doc-src/IsarRef/logics.tex	Wed Jan 09 08:33:01 2008 +0100
+++ b/doc-src/IsarRef/logics.tex	Wed Jan 09 08:57:12 2008 +0100
@@ -435,21 +435,21 @@
 
 \subsection{Recursive functions}\label{sec:recursion}
 
-\indexisarcmdof{HOL}{primrec}
+\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{fun}\indexisarcmdof{HOL}{function}\indexisarcmdof{HOL}{termination}
 
 \begin{matharray}{rcl}
-  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
-  \isarcmd{fun} & : & \isartrans{theory}{theory} \\
-  \isarcmd{function} & : & \isartrans{theory}{proof(prove)} \\
-  \isarcmd{termination} & : & \isartrans{theory}{proof(prove)} \\
+  \isarcmd{primrec} & : & \isarkeep{local{\dsh}theory} \\
+  \isarcmd{fun} & : & \isarkeep{local{\dsh}theory} \\
+  \isarcmd{function} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
+  \isarcmd{termination} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
 \end{matharray}
 
 \railalias{funopts}{function\_opts}
 
 \begin{rail}
-  'primrec' parname? (equation +)
+  'primrec' target? fixes 'where' equations
   ;
-  equation: thmdecl? prop
+  equations: (thmdecl? prop + '|')
   ;
   ('fun' | 'function') (funopts)? fixes 'where' clauses
   ;
@@ -462,10 +462,10 @@
 \end{rail}
 
 \begin{descr}
-  
+
 \item [$\isarkeyword{primrec}$] defines primitive recursive functions over
   datatypes, see also \cite{isabelle-HOL}.
-  
+
 \item [$\isarkeyword{function}$] defines functions by general
   wellfounded recursion. A detailed description with examples can be
   found in \cite{isabelle-function}. The function is specified by a
@@ -718,10 +718,10 @@
 
 \indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{inductive-set}\indexisarcmdof{HOL}{coinductive}\indexisarcmdof{HOL}{coinductive-set}\indexisarattof{HOL}{mono}
 \begin{matharray}{rcl}
-  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
-  \isarcmd{inductive_set} & : & \isartrans{theory}{theory} \\
-  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
-  \isarcmd{coinductive_set} & : & \isartrans{theory}{theory} \\
+  \isarcmd{inductive} & : & \isarkeep{local{\dsh}theory} \\
+  \isarcmd{inductive_set} & : & \isarkeep{local{\dsh}theory} \\
+  \isarcmd{coinductive} & : & \isarkeep{local{\dsh}theory} \\
+  \isarcmd{coinductive_set} & : & \isarkeep{local{\dsh}theory} \\
   mono & : & \isaratt \\
 \end{matharray}