# HG changeset patch
# User wenzelm
# Date 975611089 -3600
# Node ID 5e19ae8d9582e9394326c0a1b96990ef19f5b615
# Parent  e8c774c121058de417aaf7a031ccb22a34f67c93
cases/induct: tuned handling of facts ('consumes');

diff -r e8c774c12105 -r 5e19ae8d9582 doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Thu Nov 30 20:04:16 2000 +0100
+++ b/doc-src/IsarRef/hol.tex	Thu Nov 30 20:04:49 2000 +0100
@@ -208,7 +208,7 @@
 \end{rail}
 
 
-\section{(Co)Inductive sets}
+\section{(Co)Inductive sets}\label{sec:inductive}
 
 \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono}
 \begin{matharray}{rcl}
@@ -367,8 +367,24 @@
 $\vec\phi$.  Also note that local definitions may be expressed as $\All{\vec
   x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
 
+\medskip
 
-\subsection{Declaring rules}
+Facts presented to either method are consumed according to the number of
+``major premises'' of the rule involved (see also \S\ref{sec:induct-att} and
+\S\ref{sec:cases}), which is usually $0$ for plain cases and induction rules
+of datatypes etc.\ and $1$ for rules of inductive sets and the like.  The
+remaining facts are inserted into the goal verbatim before the actual $cases$
+or $induct$ rule is applied (thus facts may be even passed through an
+induction).
+
+Note that whenever facts are present, the default rule selection scheme would
+provide a ``set'' rule only, with the first fact consumed and the rest
+inserted into the goal.  In order to pass all facts into a ``type'' rule
+instead, one would have to specify this explicitly, e.g.\ by appending
+``$type: name$'' to the method argument.
+
+
+\subsection{Declaring rules}\label{sec:induct-att}
 
 \indexisaratt{cases}\indexisaratt{induct}
 \begin{matharray}{rcl}
@@ -394,6 +410,10 @@
 Refer to the $case_names$ and $params$ attributes (see \S\ref{sec:cases}) to
 adjust names of cases and parameters of a rule.
 
+The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of
+automatically (if none had been given already): $consumes~0$ is specified for
+``type'' rules and $consumes~1$ for ``set'' rules.
+
 
 \subsection{Emulating tactic scripts}\label{sec:induct_tac}