split Type_Infer into early and late part, after Proof_Context; added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;

minor tuning and modernization;

slightly more special eq_list/eq_set, with shortcut involving pointer_eq;

simplified check/uncheck interfaces: result comparison is hardwired by default; tuned;

updated some theory primitives, which now depend on auxiliary context;

more precise treatment of existing type inference parameters; tuned;

pretty_abbrev: read abbreviation more directly;

tuned signature;

raised timeouts further, for SML/NJ!

Package prefix is now taken into account when looking up user-defined types and proof functions.

merged

recovered Theory.check_def: full name needs to be determined from background thy, not auxiliary ctxt (broken in 774df7c59508, caused Nitpick.all_axioms_of to produce bad results);

scheduler for Mutabelle regression

tool for importing nightly isatest logs

adding bounded_forall tester

creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned

pass plain Proof.context for pretty printing;

standardized aliases of operations on tsig;

pass plain Proof.context for pretty printing;

tuned;

simplified Sorts.class_error: plain Proof.context; tuned;

pass plain Proof.context for pretty printing;

simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;

provide structure Syntax early (before structure Type), back-patch check/uncheck later;

added Binding.print convenience, which includes quote already;

markup attributes/methods via name space; eliminated obsolete markup;

tuned signature;

markup facts via name space; eliminated obsolete markup;

tuned -- order in memory according to variance;

eliminated obsolete markup -- superseded by generic "entity" markup;

report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;

clarified pretty_parsetree: suppress literal tokens;

PARALLEL_GOALS for simplification within auto_tac;

PARALLEL_GOALS for method "simp_all";

enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);

refined PARALLEL_GOALS;

tuned blast: navigate to subgoal only once;

proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way; tuned;

more direct Thm.cprem_of (with exception THM instead of Subscript); modernized thy;

more direct Thm.cprem_of (with exception THM instead of Subscript);

more direct Logic.dest_implies (with exception TERM instead of Subscript);

eliminated old List.nth; tuned;

do not open ML structures;

observe firm naming convention ctxt: Proof.context;

modernized structure Proof_Context;

modernized structure Proof_Context;

prefer local name spaces; tuned signatures; tuned;

Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;

tuned signature, disentangled dependencies;

Added command for associating user-defined types with SPARK types.

turn YXML.parse_file into a fold

nicer error message from Metis for know failure that isn't the user's fault

correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"

tuning

remove needless export

more clausification tests

make 48170228f562 work also with "HO_Reas" examples

improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)

properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code

remove experimental code added in 85bb6fbb8e6a