* 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/FuncSet.thy: Extended support for Pi and extensional and introduce the extensional dependent function space "PiE". Replaces extensional_funcset by an abbreviation, rename a couple of lemmas from extensional_funcset to PiE: extensional_empty ~> PiE_empty extensional_funcset_empty_domain ~> PiE_empty_domain extensional_funcset_empty_range ~> PiE_empty_range extensional_funcset_arb ~> PiE_arb extensional_funcset_mem > PiE_mem extensional_funcset_extend_domainI ~> PiE_fun_upd extensional_funcset_restrict_domain ~> fun_upd_in_PiE extensional_funcset_extend_domain_eq ~> PiE_insert_eq card_extensional_funcset ~> card_PiE finite_extensional_funcset ~> finite_PiE * Library/Countable_Set.thy: Theory of countable sets. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev