made "neg_clausify" a legacy feature

kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output

redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs

fix bugs in Sledgehammer's Isar proof "redirection" code

handle Vampire's definitions smoothly

fix bug in direct Isar proofs, which was exhibited by the "BigO" example

honor "xsymbols"

kill another neg_clausify proof

show types in Isar proofs, but not for free variables; this makes proofs more robust, without as much clutter as there used to be when types were enabled previously

give more helpful error message

first proposal for a announcement

NEWS (more strict internal axioms/defs format)

one all-inclusive bundle for each platform;

more robust handling of additional type variables: warning, more canonical order, drop mixfix syntax if implicit type arguments are introduced (to avoid delusion due to shifted arguments);

tuned warning;

less ambitious settings;

spelling;

do not open Proofterm, which is very ould style;

eliminated ML structure alias;

tuned default perspective;

tracing in aliceblue;

discontinued obsolete Isar.context() -- long superseded by @{context};

diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};

allow qualified names;

CONTRIBUTORS

clarified

mention unconstrain in NEWS

merged

hide default, map_entry, map_default

improved parallelism of proof term normalization;