# HG changeset patch
# User wenzelm
# Date 1357730529 -3600
# Node ID 15dc91cf47502d37c3e847d15ca7b455cbf7421f
# Parent  20126dd9772c973118879a6878acfd9e6c66f1e7
tune spelling;

diff -r 20126dd9772c -r 15dc91cf4750 NEWS
--- 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
diff -r 20126dd9772c -r 15dc91cf4750 src/Doc/IsarRef/Proof.thy
--- 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