1.1 --- a/NEWS	Wed May 02 19:02:16 2012 +0200
     1.2 +++ b/NEWS	Wed May 02 20:15:31 2012 +0200
     1.3 @@ -814,14 +814,14 @@
     1.4  defined in HOL/Word/WordBitwise.thy.  Supports addition, subtraction,
     1.5  multiplication, shifting by constants, bitwise operators and numeric
     1.6  constants.  Requires fixed-length word types, not 'a word.  Solves
     1.7 -many standard word identies outright and converts more into first
     1.8 +many standard word identities outright and converts more into first
     1.9  order problems amenable to blast or similar.  See also examples in
    1.10  HOL/Word/Examples/WordExamples.thy.
    1.11  
    1.12  * Session HOL-Probability: Introduced the type "'a measure" to
    1.13  represent measures, this replaces the records 'a algebra and 'a
    1.14  measure_space.  The locales based on subset_class now have two
    1.15 -locale-parameters the space \<Omega> and the set of measurables sets
    1.16 +locale-parameters the space \<Omega> and the set of measurable sets
    1.17  M.  The product of probability spaces uses now the same constant as
    1.18  the finite product of sigma-finite measure spaces "PiM :: ('i => 'a)
    1.19  measure".  Most constants are defined now outside of locales and gain