more graceful failure if some of the involved BNFs have no data

sort BNFs in output

preserve order of type arguments in pre-FP BNF typedef

register pre-fixpoint BNFs in database to enable lookup later (e.g. in 'corec')

store low-level (un)fold constants

export more functions

restored broken metis proof

distributivity of partial minus establishes desired properties of dvd in semirings

explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation

modernized

more multiset theorems

semantic completion for @{system_option};

clarified position;

HOL-SPARK .prv files are subject to system option spark_prv; tuned;

tuned signature;

NEWS;

prefer local fixes;

proper signature; tuned;

dummies may depend on goal params as well;

merged

proper comparison of blobs_info (amending illtyped equality from 86a76300137e) -- avoid redundant update of unchanged commands;

clarified case_tac fixes and context;

clarified name;

option to control old-style schematic mode;

clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;

tuned;

tuned proof;

admit dummy patterns in instantiations; clarified context;

clarified input source;

tuning