more accurate resolution of hybrid facts, which actually changes the sort order of results;

tuned -- command 'text' was localized some years ago;

back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;

just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.); more thorough background_notes: distribute global notes to all contexts;

more frugal recording of changes: join merely requires information from one side; tuned;

do not test details of error messages;

minor tuning -- NB: props are usually empty for global facts;

even smarter Path.smart_implode;

added ML antiquotation @{path};

clarified Path.smart_implode; more informative report and rendering;

generalization of differential_zero_maxmin to class real_normed_vector

delayed construction of command (and of noncommercial check) + tuning

tuning

consolidate consecutive steps that prove the same formula

remove '__' skolem suffixes before showing terms to users

undo rewrite rules (e.g. for 'fun_app') in Isar

debugging stuff

more simplification of trivial steps

tuning

tuned wording (pun)

document the new 'nonexhaustive' option (cf. 52e8f110fec3)

made SML/NJ happier

print warning if some constructors are missing; make this warning optional via "(nonexhaustive)"

updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'

updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit

updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)

remove ordered_euclidean_space constraint from brouwer/derivative lemmas; add constant unit_cube for class euclidean_space

typos

merged

tuned tactics