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

author | hoelzl |

Wed, 21 Nov 2012 10:57:50 +0100 | |

changeset 50141 | 15523888c11b |

parent 50140 | 74773e3dc85d |

child 50142 | bc82d25af543 |

NEWS: document changes in HOL-Probability

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