diff -r 50ca726466c6 -r 0a604b2fc2b1 doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/IsarRef/hol.tex	Sun Oct 31 20:11:23 1999 +0100
@@ -1,6 +1,27 @@
 
 \chapter{Isabelle/HOL Tools and Packages}\label{ch:hol-tools}
 
+\section{Miscellaneous attributes}
+
+\indexisaratt{rulify}\indexisaratt{rulify-prems}
+\begin{matharray}{rcl}
+  rulify & : & \isaratt \\
+  rulify_prems & : & \isaratt \\
+\end{matharray}
+
+\begin{descr}
+
+\item [$rulify$] puts a theorem into object-rule form, replacing implication
+  and universal quantification of HOL by the corresponding meta-logical
+  connectives.  This is the same operation as performed by the
+  \texttt{qed_spec_mp} ML function.
+  
+\item [$rulify_prems$] is similar to $rulify$, but acts on the premises of a
+  rule.
+
+\end{descr}
+
+
 \section{Primitive types}
 
 \indexisarcmd{typedecl}\indexisarcmd{typedef}
@@ -119,9 +140,11 @@
 \section{(Co)Inductive sets}
 
 \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive-cases}
+\indexisaratt{mono}
 \begin{matharray}{rcl}
   \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
   \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
+  mono & : & \isaratt \\
   \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
@@ -136,11 +159,16 @@
   ;
   indcases thmdef? nameref ':' \\ (prop +) comment?
   ;
+  'mono' (() | 'add' | 'del')
+  ;
 \end{rail}
 
 \begin{descr}
 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
   (co)inductive sets from the given introduction rules.
+\item [$mono$] adds or deletes monotonicity rules from the theory or proof
+  context (the default is to add).  These rule are involved in the automated
+  monotonicity proof of $\isarkeyword{inductive}$.
 \item [$\isarkeyword{inductive_cases}$] creates simplified instances of
   elimination rules of (co)inductive sets.
 \end{descr}