tuned spelling;
Wed, 02 May 2012 20:15:31 +0200
changeset 47854 94c5aaf32269
parent 47853 c01ba36769f5
child 47855 1246d847b8c1
tuned spelling;
--- a/NEWS	Wed May 02 19:02:16 2012 +0200
+++ b/NEWS	Wed May 02 20:15:31 2012 +0200
@@ -814,14 +814,14 @@
 defined in HOL/Word/WordBitwise.thy.  Supports addition, subtraction,
 multiplication, shifting by constants, bitwise operators and numeric
 constants.  Requires fixed-length word types, not 'a word.  Solves
-many standard word identies outright and converts more into first
+many standard word identities outright and converts more into first
 order problems amenable to blast or similar.  See also examples in
 * Session HOL-Probability: Introduced the type "'a measure" to
 represent measures, this replaces the records 'a algebra and 'a
 measure_space.  The locales based on subset_class now have two
-locale-parameters the space \<Omega> and the set of measurables sets
+locale-parameters the space \<Omega> and the set of measurable sets
 M.  The product of probability spaces uses now the same constant as
 the finite product of sigma-finite measure spaces "PiM :: ('i => 'a)
 measure".  Most constants are defined now outside of locales and gain