[isabelle-dev] NEWS

[Johannes Hölzl]

* 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.