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;

tuned signature;

merged

removing decrement of cardinality in quickcheck -- counting cardinalities starts at 1

removing instantiation exhaustive for unit in Quickcheck_Exhaustive

correcting bounded_forall construction; tuned

dropped unused lemmas; proper Isar proof

further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind

make new Skolemizer more robust

tuned comment

discontinued user-defined token translations; tuned signature;

simplified printer context: uniform externing and static token translations;

clarified Pretty.mark; added Pretty.mark_str, Pretty.marks_str convenience;