reworked Probability theory: measures are not type restricted to positive extended reals

split Extended_Reals into parts for Library and Multivariate_Analysis

lemmas about addition, SUP on countable sets and infinite sums for extreal

add infinite sums and power on extreal

introduce setsum on extreal

use abs_extreal

simplified definition of open_extreal

use case_product for extrel[2,3]_cases

add Extended_Reals from AFP/Lower_Semicontinuous

add lemmas for monotone sequences

add lemmas for SUP and INF

generalize infinite sums

moved t2_spaces to HOL image

example settings for ISABELLE_GHC, ISABELLE_OCAML, ISABELLE_SWIPL;

isatest: fresh copy of settings avoids odd cumulative environment;

tuned exhaustive_generators

removing definition of cons0; hiding constants in Quickcheck_Narrowing

tuned subsubsection names in Quickcheck_Narrowing

tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)

correcting names in Narrowing_Engine and example theory for Quickcheck_Narrowing

renaming series and serial to narrowing in Quickcheck_Narrowing

eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;

tuned headers;

eliminated hard tabs;

less ambitious isatest;

modernized imports (untested!?);

files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;

explicit type SHA1.digest;