doc-src/IsarRef/hol.tex
 changeset 7990 0a604b2fc2b1 parent 7987 d9aef93c0e32 child 8449 f8ff23736465
     1.1 --- a/doc-src/IsarRef/hol.tex	Sun Oct 31 15:26:37 1999 +0100
1.2 +++ b/doc-src/IsarRef/hol.tex	Sun Oct 31 20:11:23 1999 +0100
1.3 @@ -1,6 +1,27 @@
1.4
1.5  \chapter{Isabelle/HOL Tools and Packages}\label{ch:hol-tools}
1.6
1.7 +\section{Miscellaneous attributes}
1.8 +
1.9 +\indexisaratt{rulify}\indexisaratt{rulify-prems}
1.10 +\begin{matharray}{rcl}
1.11 +  rulify & : & \isaratt \\
1.12 +  rulify_prems & : & \isaratt \\
1.13 +\end{matharray}
1.14 +
1.15 +\begin{descr}
1.16 +
1.17 +\item [$rulify$] puts a theorem into object-rule form, replacing implication
1.18 +  and universal quantification of HOL by the corresponding meta-logical
1.19 +  connectives.  This is the same operation as performed by the
1.20 +  \texttt{qed_spec_mp} ML function.
1.21 +
1.22 +\item [$rulify_prems$] is similar to $rulify$, but acts on the premises of a
1.23 +  rule.
1.24 +
1.25 +\end{descr}
1.26 +
1.27 +
1.28  \section{Primitive types}
1.29
1.30  \indexisarcmd{typedecl}\indexisarcmd{typedef}
1.31 @@ -119,9 +140,11 @@
1.32  \section{(Co)Inductive sets}
1.33
1.34  \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive-cases}
1.35 +\indexisaratt{mono}
1.36  \begin{matharray}{rcl}
1.37    \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
1.38    \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
1.39 +  mono & : & \isaratt \\
1.40    \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
1.41  \end{matharray}
1.42
1.43 @@ -136,11 +159,16 @@
1.44    ;
1.45    indcases thmdef? nameref ':' \\ (prop +) comment?
1.46    ;
1.47 +  'mono' (() | 'add' | 'del')
1.48 +  ;
1.49  \end{rail}
1.50
1.51  \begin{descr}
1.52  \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
1.53    (co)inductive sets from the given introduction rules.
1.54 +\item [$mono$] adds or deletes monotonicity rules from the theory or proof
1.55 +  context (the default is to add).  These rule are involved in the automated
1.56 +  monotonicity proof of $\isarkeyword{inductive}$.
1.57  \item [$\isarkeyword{inductive_cases}$] creates simplified instances of
1.58    elimination rules of (co)inductive sets.
1.59  \end{descr}