tuned names

eta-expand all search patterns using schematic place holders

revert "better" handling of abbreviation from c61fe520602b

tuned variable names

turn application-specific Pattern.matches_subterm into an application-private function

cleaned up mess

add Poisson and Binomial distribution

add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav

proper GUI_Thread context (cf. 7e0d3da6e6d8);

more examples;

tuned header;

generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces

merged

node-specific keywords, with session base syntax as default;

clarified define_command: send tokens more directly, without requiring keywords in ML;

more robust bundle_name: avoid assumptions about identifier, keywords etc.;

tuned signature;

tuned;

clarified token kind;

added Untyped.method convenience (for *this* class only);

tuned signature -- more explicit types;

more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;

node-specific syntax, with base_syntax as default; clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;

clarified token marker / syntax for mode vs. buffer;

Sidekick syntax is derived from buffer (and its mode), instead of parser name;

tuned signature;

more merge operations;

tuned signature;

tuned;

prefer E 1.8, now that it's been tried and tested

more accurate context;

update_cartouches;

tuned signature;

tuned signature;

tuned signature -- prefer Input.source;

more abstract type Input.source;

encode text with control symbols;

proper HTML.encode;

prefer abbrev for is_unit

do not conceal inductive predicate names properly, following 4a3747517552

tuned

renamed "pairself" to "apply2", in accordance to @{apply 2};

added ML antiquotation @{apply n} or @{apply n(k)};

even more exception traces for Document.update, which goes through additional execution wrappers;

more informative failure of protocol commands, with exception trace; eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);

load simple_thread.ML later, such that it benefits from redefined print_exception_trace;

tuned proof that pmfs are bnfs

projections of pair_pmf (by D. Traytel)

merged

removed odd remains of structural containment checks, which stem from an older approach (see also 3ad1b289f21b, 3ae3cc4b1eac, 423af2e013b8, bad13b32c0f3, ccd6de95f4a6); de-facto this alternative never occured in practice, but it can lead to non-termination of the check;

preinstantiate (co)inductions in N2M to handle mutual but separated SCCs

add congruence solver to measurability prover

cleanup measurability prover

updated SMT certificates

added one more CVC4 option that helps Judgment Day (10 theory version)

tuned whitespace

keep all 'ctr' theorems

smoothly handle unit codatatypes in 'primcorec'

careful with de Bruijn indices

improved message in 'co' case

updated NEWS

no need for subset operation as a primitive in Nitpick, esp. that its implementation was unsound (cf. Rene Thiemann's 16 Oct 2014 email on isabelle mailing list)

added Z3 reconstruction rule suggested by F. Maric

one more CVC4 option that helps