clarified Consts.read_const;

clarified Type.the_decl;

more reports and error positions;

added Name_Space.check/get convenience;

clarified check_simproc (with report) vs. the_simproc; proper report for @{simproc} (NB: ML environment is built in invisible context); only one data slot for this module;

proper binding/report of defined simprocs; tuned signature;

modernized specifications;

tuned signature;

stats for mac-poly-M2;

simplified Data signature;

misc tuning and simplification;

misc tuning;

do not open ML structures;

proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61); tuned signature;

modernized Quantifier1 simproc setup;

tuned signature;

clarified simpset setup; discontinued unused old-style FOL_css;

iterate the unsound-fact-set removal process to recover even more unsound proofs

automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option

automatically retry with full-types upon unsound proof

detect some unsound proofs before showing them to the user

tuning -- local semicolon consistency

tuning

rewording

fixed interaction between monomorphization and slicing for ATPs

cleanup: get rid of "may_slice" arguments without changing semantics

implemented general slicing for ATPs, especially E 1.2w and above

fixed typo in documentation

more robust scanning of iterated comments, such as "(* (**) (**) *)";

discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;