tuned signature; tuned;

bundle lifting_syntax;

tuned;

clarified derived bindings (for PIDE reports);

clarified rendering (amending ae9330fdbc16);

tuned whitespace;

merged

position information for literal facts; Markup.entry may have empty kind/name;

tuned;

tuned;

Multivariate_Analysis: add continuous_on_vec_lambda

Probability: show that measures form a complete lattice

move open_Collect_eq/less to HOL

move Conditional_Complete_Lattices to Main

Probability: introduce Hahn decomposition; use it to clean up Radon_Nikodym

Probability: tuned headers; cleanup Radon_Nikodym

read Java system properties from ISABELLE_CI_PROPERTIES

merged

misc tuning and modernization;

misc tuning and modernization;

prefer HOL definitions;

tuned proof;

misc tuning and modernization;

Merged

Merged

fps_from_poly → fps_of_poly

Merged

Various additions to polynomials, FPSs, Gamma function

misc tuning and modernization;

benchmark build profile

killed dead code

avoid runtime warning with discriminators due to 'Code.del_eqn'

killed deadcode

be more careful before filtering out chained facts in Sledgehammer

normalising multiset theorem names

tuned;

isabelle update_cartouches -c -t;

tuned;

Removed instances of ^ from theory markup

Urysohn's lemma, Dugundji extension theorem and many other proofs

non-deprecated char literals for Scala

explicit resolution of ambiguous dictionaries

Merge

new results about topology

Merged

Integration by substitution

tuned;

tuned;

Integral form of Gamma function

Facts about HK integration, complex powers, Gamma function

tuned

tuned;

tuned;

tuned;

boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes

merged

start moving actual Jenkins build scripts into the repository

tuned order for isar-ref;

clarified;

clarified syntax;

spelling;

bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;

added command 'unbundle';

Merge

code to catch exception TERM in blast

merged

avoid duplicate Attrib.local_notes in aux. context;

proper restore;

tuned;

tuned;

tuned;

prefer hybrid 'bundle' command;

documentation;

clarified;

support for bundle definition via target;

tuned signature;

tuned;

tuned signature;

tuned;

Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.

merged

approximation, derivative, and continuity of floor and ceiling

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