tune spelling;
authorwenzelm
Wed Jan 09 12:22:09 2013 +0100 (2013-01-09)
changeset 5077815dc91cf4750
parent 50777 20126dd9772c
child 50779 6f571f6797bd
child 50781 a0f22c2d60cc
tune spelling;
NEWS
src/Doc/IsarRef/Proof.thy
     1.1 --- a/NEWS	Tue Jan 08 21:16:51 2013 +0100
     1.2 +++ b/NEWS	Wed Jan 09 12:22:09 2013 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4  and "class ... context ...".
     1.5  
     1.6  * Attribute "consumes" allows a negative value as well, which is
     1.7 -interpreted relatively to the total number if premises of the rule in
     1.8 +interpreted relatively to the total number of premises of the rule in
     1.9  the target context.  This form of declaration is stable when exported
    1.10  from a nested 'context' with additional assumptions.  It is the
    1.11  preferred form for definitional packages, notably cases/rules produced
     2.1 --- a/src/Doc/IsarRef/Proof.thy	Tue Jan 08 21:16:51 2013 +0100
     2.2 +++ b/src/Doc/IsarRef/Proof.thy	Wed Jan 09 12:22:09 2013 +0100
     2.3 @@ -1247,7 +1247,7 @@
     2.4    consumes}~@{text 0} had been specified.
     2.5  
     2.6    A negative @{text n} is interpreted relatively to the total number
     2.7 -  if premises of the rule in the target context.  Thus its absolute
     2.8 +  of premises of the rule in the target context.  Thus its absolute
     2.9    value specifies the remaining number of premises, after subtracting
    2.10    the prefix of major premises as indicated above. This form of
    2.11    declaration has the technical advantage of being stable under more