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