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}