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;

slightly more robust bash exec, which fails on empty executable;

cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection; determine swipl_version at runtime;

some cleanup of old-style settings;

clarified ISABELLE_CSDP setting (formerly CSDP_EXE);

more conventional Mutabelle settings -- similar to Mirabelle;

more basic use of Path.position/File.read;

prefer qualified ISABELLE_NEOS_SERVER;

proper File.shell_path;