--- a/NEWS Tue Jan 08 16:01:07 2013 +0100
+++ b/NEWS Tue Jan 08 16:23:07 2013 +0100
@@ -38,6 +38,13 @@
specifications: nesting of "context fixes ... context assumes ..."
and "class ... context ...".
+* Attribute "consumes" allows a negative value as well, which is
+interpreted relatively to the total number if premises of the rule in
+the target context. This form of declaration is stable when exported
+from a nested 'context' with additional assumptions. It is the
+preferred form for definitional packages, notably cases/rules produced
+in HOL/inductive and HOL/function.
+
* More informative error messages for Isar proof commands involving
lazy enumerations (method applications etc.).
--- a/src/Doc/IsarRef/Proof.thy Tue Jan 08 16:01:07 2013 +0100
+++ b/src/Doc/IsarRef/Proof.thy Tue Jan 08 16:23:07 2013 +0100
@@ -1197,7 +1197,7 @@
;
@@{attribute params} ((@{syntax name} * ) + @'and')
;
- @@{attribute consumes} @{syntax nat}?
+ @@{attribute consumes} @{syntax int}?
"}
\begin{description}
@@ -1245,7 +1245,15 @@
\secref{sec:hol-inductive}). Rules without any @{attribute
consumes} declaration given are treated as if @{attribute
consumes}~@{text 0} had been specified.
-
+
+ A negative @{text n} is interpreted relatively to the total number
+ if premises of the rule in the target context. Thus its absolute
+ value specifies the remaining number of premises, after subtracting
+ the prefix of major premises as indicated above. This form of
+ declaration has the technical advantage of being stable under more
+ morphisms, notably those that export the result from a nested
+ @{command_ref context} with additional assumptions.
+
Note that explicit @{attribute consumes} declarations are only
rarely needed; this is already taken care of automatically by the
higher-level @{attribute cases}, @{attribute induct}, and
--- a/src/Pure/Isar/attrib.ML Tue Jan 08 16:01:07 2013 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Jan 08 16:23:07 2013 +0100
@@ -391,7 +391,7 @@
"rename bound variables in abstractions" #>
setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
setup (Binding.name "folded") folded "folded definitions" #>
- setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.nat 1) >> Rule_Cases.consumes)
+ setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
"number of consumed facts" #>
setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
"number of equality constraints" #>