# HG changeset patch
# User wenzelm
# Date 968772881 -7200
# Node ID a87965201c345f82aa1c0299ce4d0a95fa36b0ee
# Parent  aea053733eb0be734771252f9dce7ae74628ddd6
tuned;

diff -r aea053733eb0 -r a87965201c34 doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Tue Sep 12 17:01:14 2000 +0200
+++ b/doc-src/IsarRef/hol.tex	Tue Sep 12 17:34:41 2000 +0200
@@ -123,33 +123,18 @@
 \section{Recursive functions}
 
 \indexisarcmd{primrec}\indexisarcmd{recdef}
-\indexisaratt{recdef-simp}\indexisaratt{recdef-cong}\indexisaratt{recdef-wf}
 \begin{matharray}{rcl}
   \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
   \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
-  recdef_simp & : & \isaratt \\
-  recdef_cong & : & \isaratt \\
-  recdef_wf & : & \isaratt \\
 %FIXME
 %  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
-\railalias{recdefsimp}{recdef\_simp}
-\railterm{recdefsimp}
-
-\railalias{recdefcong}{recdef\_cong}
-\railterm{recdefcong}
-
-\railalias{recdefwf}{recdef\_wf}
-\railterm{recdefwf}
-
 \begin{rail}
   'primrec' parname? (equation + )
   ;
   'recdef' name term (eqn + ) hints?
   ;
-  (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
-  ;
 
   equation: thmdecl? eqn
   ;
@@ -170,9 +155,6 @@
   internal automated proof process of TFL; the other declarations refer to the
   Simplifier and Classical reasoner (\S\ref{sec:simplifier},
   \S\ref{sec:classical}, \S\ref{sec:clasimp}) that are used internally.
-
-\item [$recdef_simps$, $recdef_cong$, and $recdef_wf$] declare global hints
-  for $\isarkeyword{recdef}$.
 \end{descr}
 
 Both kinds of recursive definitions accommodate reasoning by induction (cf.\ 
@@ -188,6 +170,30 @@
 $\isarkeyword{recdef}$ each specification given by the user may result in
 several theorems.
 
+\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
+the following attributes.
+
+\indexisaratt{recdef-simp}\indexisaratt{recdef-cong}\indexisaratt{recdef-wf}
+\begin{matharray}{rcl}
+  recdef_simp & : & \isaratt \\
+  recdef_cong & : & \isaratt \\
+  recdef_wf & : & \isaratt \\
+\end{matharray}
+
+\railalias{recdefsimp}{recdef\_simp}
+\railterm{recdefsimp}
+
+\railalias{recdefcong}{recdef\_cong}
+\railterm{recdefcong}
+
+\railalias{recdefwf}{recdef\_wf}
+\railterm{recdefwf}
+
+\begin{rail}
+  (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
+  ;
+\end{rail}
+
 
 \section{(Co)Inductive sets}