# HG changeset patch
# User wenzelm
# Date 975611056 -3600
# Node ID e8c774c121058de417aaf7a031ccb22a34f67c93
# Parent  efaba354b7f1294eebe879b642ffa4f44f488961
'consumes' att;

diff -r efaba354b7f1 -r e8c774c12105 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Thu Nov 30 20:03:39 2000 +0100
+++ b/doc-src/IsarRef/generic.tex	Thu Nov 30 20:04:16 2000 +0100
@@ -140,12 +140,13 @@
 \section{Named local contexts (cases)}\label{sec:cases}
 
 \indexisarcmd{case}\indexisarcmd{print-cases}
-\indexisaratt{case-names}\indexisaratt{params}
+\indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
 \begin{matharray}{rcl}
   \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
   \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
   case_names & : & \isaratt \\
   params & : & \isaratt \\
+  consumes & : & \isaratt \\
 \end{matharray}
 
 Basically, Isar proof contexts are built up explicitly using commands like
@@ -186,6 +187,8 @@
   ;
   'params' ((name * ) + 'and')
   ;
+  'consumes' nat?
+  ;
 \end{rail}
 %FIXME bug in rail
 
@@ -205,6 +208,17 @@
 
   Note that the default usage of case rules does \emph{not} directly expose
   parameters to the proof context (see also \S\ref{sec:induct-method-proper}).
+\item [$consumes~n$] declares the number of ``major premises'' of a rule,
+  i.e.\ the number of facts to be consumed when it is applied by an
+  appropriate proof method (cf.\ \S\ref{sec:induct-method}).  The default
+  value of $consumes$ is $n = 1$, which is appropriate for the usual kind of
+  cases and induction rules for inductive sets (cf.\ \S\ref{sec:inductive}).
+  Rules without any $consumes$ declaration given are treated as if
+  $consumes~0$ had been specified.
+  
+  Note that explicit $consumes$ declarations are only rarely needed; this is
+  already taken care of automatically by the higher-level $cases$ and $induct$
+  declarations, see also \S\ref{sec:induct-att}.
 \end{descr}