# HG changeset patch
# User wenzelm
# Date 941397083 -3600
# Node ID 0a604b2fc2b1df524a3cf81f5a7b2255b19fda92
# Parent  50ca726466c6bf7bd28dab745e2eba1279b38737
updated;

diff -r 50ca726466c6 -r 0a604b2fc2b1 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/IsarRef/generic.tex	Sun Oct 31 20:11:23 1999 +0100
@@ -61,6 +61,7 @@
 \indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
 \indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
 \indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
+\indexisaratt{unfold}\indexisaratt{fold}
 \begin{matharray}{rcl}
   tag & : & \isaratt \\
   untag & : & \isaratt \\[0.5ex]
@@ -69,10 +70,12 @@
   COMP & : & \isaratt \\[0.5ex]
   of & : & \isaratt \\
   where & : & \isaratt \\[0.5ex]
+  unfold & : & \isaratt \\
+  fold & : & \isaratt \\[0.5ex]
   standard & : & \isaratt \\
   elimify & : & \isaratt \\
   export^* & : & \isaratt \\
-  transfer & : & \isaratt \\
+  transfer & : & \isaratt \\[0.5ex]
 \end{matharray}
 
 \begin{rail}
@@ -86,6 +89,8 @@
   ;
   'where' (name '=' term * 'and')
   ;
+  ('unfold' | 'fold') thmrefs
+  ;
 
   inst: underscore | term
   ;
@@ -108,7 +113,12 @@
 \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
   instantiation, respectively.  The terms given in $of$ are substituted for
   any schematic variables occurring in a theorem from left to right;
-  ``\texttt{_}'' (underscore) indicates to skip a position.
+  ``\texttt{_}'' (underscore) indicates to skip a position.  Arguments
+  following a ``$concl\colon$'' specification refer to positions of the
+  conclusion of a rule.
+  
+\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
+  meta-level definitions throughout a rule.
  
 \item [$standard$] puts a theorem into the standard form of object-rules, just
   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
@@ -447,7 +457,8 @@
 \item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
   respectively.  By default, rules are considered as \emph{safe}, while a
   single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\ 
-  not applied in the search-oriented automated methods, but only $rule$).
+  not applied in the search-oriented automated methods, but only in
+  single-step methods such as $rule$).
   
 \item [$iff$] declares equations both as rewrite rules for the simplifier and
   classical reasoning rules.
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}
diff -r 50ca726466c6 -r 0a604b2fc2b1 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/Ref/classical.tex	Sun Oct 31 20:11:23 1999 +0100
@@ -670,6 +670,17 @@
 \end{ttbox}
 deletes rules from the current claset. 
 
+\medskip A few further functions are available as uppercase versions only:
+\begin{ttbox}
+AddXIs, AddXEs, AddXDs: thm list -> unit
+\end{ttbox}
+\indexbold{*AddXIs} \indexbold{*AddXEs} \indexbold{*AddXDs} augment the
+current claset by \emph{extra} introduction, elimination, or destruct rules.
+These provide additional hints for the basic non-automated proof methods of
+Isabelle/Isar \cite{isabelle-isar-ref}.  The corresponding Isar attributes are
+``$intro!!$'', ``$elim!!$'', and ``$dest!!$''.  Note that these extra rules do
+not have any effect on classic Isabelle tactics.
+
 
 \subsection{Accessing the current claset}
 \label{sec:access-current-claset}
diff -r 50ca726466c6 -r 0a604b2fc2b1 doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/Ref/goals.tex	Sun Oct 31 20:11:23 1999 +0100
@@ -186,14 +186,14 @@
   stores $thm$ in the theorem database associated with its theory and
   returns that theorem.
   
-\item[\ttindexbold{bind_thms} and \ttindexbold{store_thms}] are similar to
+\item[\ttindexbold{bind_thms} \textrm{and} \ttindexbold{store_thms}] are similar to
   \texttt{bind_thm} and \texttt{store_thm}, but store lists of theorems.
 
 \end{ttdescription}
 
-The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be empty
-(\texttt{""}) as well; in that case the result is \emph{not} stored, but
-proper checks and presentation of the result still apply.
+The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be the empty
+string as well; in that case the result is \emph{not} stored, but proper
+checks and presentation of the result still apply.
 
 
 \subsection{Extracting axioms and stored theorems}
diff -r 50ca726466c6 -r 0a604b2fc2b1 doc-src/Ref/introduction.tex
--- a/doc-src/Ref/introduction.tex	Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/Ref/introduction.tex	Sun Oct 31 20:11:23 1999 +0100
@@ -39,10 +39,10 @@
 Subsequently, we assume that the \texttt{isabelle} executable is determined
 automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
   \rangle\)/bin} to your search path.\footnote{Depending on your installation,
-  there might be also stand-alone binaries located in some global directory
-  such as \texttt{/usr/bin}.  Do not attempt to copy {\tt \(\langle
-    isabellehome \rangle\)/bin/isabelle}, though!  See \texttt{isatool
-    install} in \emph{The Isabelle System Manual} of how to do this properly.}
+  there may be stand-alone binaries located in some global directory such as
+  \texttt{/usr/bin}.  Do not attempt to copy {\tt \(\langle isabellehome
+    \rangle\)/bin/isabelle}, though!  See \texttt{isatool install} in
+  \emph{The Isabelle System Manual} of how to do this properly.}
 
 \medskip
 
diff -r 50ca726466c6 -r 0a604b2fc2b1 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/Ref/simplifier.tex	Sun Oct 31 20:11:23 1999 +0100
@@ -502,7 +502,8 @@
 
 \subsection{*The subgoaler}\label{sec:simp-subgoaler}
 \begin{ttbox}
-setsubgoaler : simpset *  (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
+setsubgoaler :
+  simpset *  (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
 prems_of_ss  : simpset -> thm list
 \end{ttbox}
 
@@ -794,7 +795,7 @@
 \end{warn}
 
 
-\section{Examples of using the simplifier}
+\section{Examples of using the Simplifier}
 \index{examples!of simplification} Assume we are working within {\tt
   FOL} (see the file \texttt{FOL/ex/Nat}) and that
 \begin{ttdescription}
@@ -1239,7 +1240,7 @@
 prove particular theorems depending on the current redex.
 
 
-\section{*Setting up the simplifier}\label{sec:setting-up-simp}
+\section{*Setting up the Simplifier}\label{sec:setting-up-simp}
 \index{simplification!setting up}
 
 Setting up the simplifier for new logics is complicated.  This section