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

added examples of definitional CNF facts

"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now

compile

handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377

removed obsolete Skolem counter in new Skolemizer

added outstanding issue to Metis example

use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms

started clausifier examples

make new Skolemizer work also for "metisFT"

improve definitional CNF on goal by moving "not" past the quantifiers

experiment with definitional CNF

use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer

try to repair out-of-sync situations in Metis

handle Vampire [predicate definition introduction] steps the same way as missing proof, since such steps do not report which axioms were used

Add YXML.parse_file to signature ...

Add YXML.parse_file to parse and process big data files

Generalized File.fold_lines to File.fold_fields

more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;

Name_Space.entry_markup: keep def position as separate properties; uniform treatment of ML_def/ML_open/ML_struct as entities; hyperlinks for all entities -- excluding ML_open/ML_struct for now;

some position reports for 'translations';

made SML/NJ happy;

merged

added SMT certificates

use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)

fixed eta-expansion: use correct order to apply new bound variables

check if negating the goal is possible (avoids CTERM exception for Pure propositions)

unfold and eta-contract let expressions before lambda-lifting to avoid bad terms

corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables

merged

deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments

generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations

correcting constant name in exhaustive_generators

switching fast compilation off by default for now in exhaustive quickcheck

ensuring datatype limitations before the instantiation in quickcheck_exhaustive

rational and real instances for new compilation scheme for exhaustive quickcheck

splitting exhaustive and full_exhaustive into separate type classes

removing duplicate code

revisiting mk_equation functions and refactoring them in exhaustive quickcheck

creating a general mk_equation_terms for the different compilations

adding an even faster compilation scheme

theory definitions for fast exhaustive quickcheck compilation

new compilation for exhaustive quickcheck

tuned;

present type variables; tuned;

unparse: more accurate markup for syntax consts, notably binders;

notation: proper markup for type constructor / constant;

tuned signature;

more accurate markup for syntax consts, notably binders which point back to the original logical entity; tuned;

discontinued Syntax.max_pri, which is not really a symbolic parameter;

CONST syntax with positions;

moved CONST syntax/translations to their proper place;

simplified Pure syntax bootstrap;

renamed sprop "prop#" to "prop'" -- proper identifier; eliminated spurious symbolic string bindings (logic, any etc.); hardwired special "prop" vs. "prop'" conversion; tuned;

merged

raised timeout further, for SML/NJ

discontinued special treatment of structure Lexicon;

discontinued special status of structure Printer;

discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root;

discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;

more antiquotations;

removed outdated text (cf. 84a3f86441eb);

explicit structure Syntax_Trans; discontinued old-style constrainAbsC;

tuned presentation;

report literal tokens according to parsetree head; some attempts to stack parsetrees in proper order;

simplified read_term vs. read_prop;

tuned signature;

constant =?= no longer exists (cf. 8c09e1fa24a7);

clarified sources -- removed odd comments;