remove smt call in Lebesge_Measure

proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);

merged

NEWS;

tuned proofs;

provide dynamic facts in static context, to allow use of method_facts during static closure;

tuned;

clarified signature;

less ambitious arguments: thms only, no context declaration;

added method operator "use";

clarified signature;

clean facts more uniformly;

expode method_facts via dynamic method context;

tuned;

generalized bitlen to floor of log

repair Unicode mess-up in c493859d4267

NEWS and CONTRIBUTORS for SPMF

merged

import wasysym needed by Rewrite.thy

add theory of discrete subprobability distributions

clear distinction between different situations concerning strictness of code equations

tuned signature

more correct exception handling

explicit tagging of code equations de-baroquifies interface

dropped unused code

conventional syntax for unit abstractions

added action "isabelle.select-entity";

tuned;

clarified focus_defs vs. focus_refs, e.g. relevant for @{here} where this overlaps;

tuned;

less redundant exploration of full name space;

tuned;

avoid multiple reports on shared type;

updated to recent changes of Poly/ML directory layout;

tuned;

Integer.lcm normalizes the sign as in HOL/GCD.thy; tuned;

support for .scala tools;

move ennreal and ereal theorems from MFMC_Countable

more flexible build_selection;

clarified aliases (no warning for duplicates);

eliminated pointless alias (no warning for duplicates);

avoid warnings on duplicate rules in the given list;

avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp;

Hid RBT.filter

proper ceil operation;

tuned;

isabelle components_checksum -u;

more documentation;

updated to jdk-8u92;

merged

NEWS;

more adhoc overloading; eliminated pointless Rat.eq: this is an equality type; tuned;

clarified exception -- actually reject denominator = 0;

ML pp for Rat.rat;

clarified string_of_rat operations;

tuned signature;

clarified signature;

prefer rat numberals;

support rat numerals via special antiquotation syntax;

tuned signature;