summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

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 HOL/Word/Examples/WordExamples.thy. * 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