tuned;

merged

clarified markup for embedded files, early before execution;

clarified command content;

tuned -- more uniform ML vs. Scala;

quote "method" to allow Eisbach using this keyword;

rel_pmf on equivalence relation

make proofs work with 4762c690a75c

add subadditivity for Liminf on ereal

merged

merged

more type class instances

documented renamed theories

export more functions (for future 'corec')

tuning

merged

more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;

generalized bind_cond_pmf_cancel

renaming HOL/Fact.thy -> Binomial.thy

Merge

Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy

clarified Token.check_src: intern at most once; Method.parse_internal for Eisbach: intern method names;

add set_pmf lemmas to simpset

build pmf's on bind

split into subgoals

tuning

merged

support structural composition (THEN_ALL_NEW) for proof methods; clarified preparation for goal restriction: Goal.conjunction_tac only once; export Method.parse0, notably for Eisbach; more explicit type cases_state;

Removed the infix operator "choose" to allow HOLCF to build

sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex

eliminated unused arith "verbose" flag -- tools that need options can use the context;

eliminated dead code (cf. 5e5c36b051af);

tuned;

clarified aliases;

misc tuning and simplification;

tuned;

misc tuning and simplification;

tuned;

cartouche_declaration for Eisbach;

NEWS;

clarified Drule.gen_all: observe context more carefully;

added declare_maxidx operations for Eisbach;

clarified Variable.export: observe maxidx of target context;

tuned;

clarified context;

clarified context;

clarified context;

clarified context;