--- a/NEWS Tue Jan 08 21:16:51 2013 +0100
+++ b/NEWS Wed Jan 09 12:22:09 2013 +0100
@@ -39,7 +39,7 @@
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
+interpreted relatively to the total number of 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
--- a/src/Doc/IsarRef/Proof.thy Tue Jan 08 21:16:51 2013 +0100
+++ b/src/Doc/IsarRef/Proof.thy Wed Jan 09 12:22:09 2013 +0100
@@ -1247,7 +1247,7 @@
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
+ of 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