author | hoelzl |

Wed Nov 21 10:57:50 2012 +0100 (2012-11-21) | |

changeset 50141 | 15523888c11b |

parent 50140 | 74773e3dc85d |

child 50142 | bc82d25af543 |

NEWS: document changes in HOL-Probability

1.1 --- a/NEWS Wed Nov 21 10:48:58 2012 +0100 1.2 +++ b/NEWS Wed Nov 21 10:57:50 2012 +0100 1.3 @@ -198,6 +198,14 @@ 1.4 * HOL/Cardinals: Theories of ordinals and cardinals 1.5 (supersedes the AFP entry "Ordinals_and_Cardinals"). 1.6 1.7 +* HOL/Probability: 1.8 + - Add simproc "measurable" to automatically prove measurability 1.9 + 1.10 + - Add induction rules for sigma sets with disjoint union (sigma_sets_induct_disjoint) 1.11 + and for Borel-measurable functions (borel_measurable_induct). 1.12 + 1.13 + - The Daniell-Kolmogorov theorem (the existence the limit of a projective family) 1.14 + 1.15 * Library/Countable_Set.thy: Theory of countable sets. 1.16 1.17 * Library/Debug.thy and Library/Parallel.thy: debugging and parallel