correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives

don't lose error messages

don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice

careful with partial applications

don't perform preplaying steps if preplaying is disabled

adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs

tuned punctuation

handle TPTP '!=' more gracefully in Isar proof reconstruction

guard against duplicate lines in Zipperposition proofs

tuning

tuned NEWS

compile HOL-TPTP

compile Metis_Examples

more NEWS

compile mirabelle

tweaked Auto Sledgehammer's behavior and output

updated NEWS

removed experimental prover z3_tptp

print more verbose information

run all installed provers by default

update slice options centrally

further work on new Sledgehammer slicing

tweaked verbose output

tweak padding of prover slice schedule to include all provers

implemented 'max_proofs' mechanism

document new option 'max_proofs'

crude implementation of centralized slicing

removed obscure E option

take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set

rationalize slicing format

thread slices through

simplified 'best_slice' data structure and made minor changes to slices

changed logic of 'slice' option to 'slices'

updated documentation of 'slice' (now 'slices') option

revised Sledgehammer documentation

rationalized output for forthcoming slicing model

use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code

disable slicing within ATP module (in preparation for refactoring)

disable slicing within SMT (in preparation for factoring it out)

generalized the 'slice' option towards more flexible slicing

tuned -- fewer warnings;

Added a tiny proof

Deletion of a duplicate proof

useful lemma integral_less

merged

removed unused parameter following f9908452b282

treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)

fixed dodgy intro! attributes

merged

optimized facts traversal in TPTP translation

optimized app_op_level selection in TPTP generation

tuned trivial check in mirabelle_sledgehammer

renamed run_action to run in Mirabelle.action record

added spying of fact filtering timing

tuned mirabelle_sledgehammer output

added spying to Sledgehammer

proper fact filter for dummy ATPs

added syping of fact filtering time to sledgehammer

removed unsynchronized references in mirabelle_sledgehammer

tuned mirabelle_sledgehammer to have a single call to Synchronized.change per run

updated to polyml-test-15c840d48c9a;

some updates and clarification on Assumption.export_term;

new theorem has_integral_UN

updated to jdk-17.0.2+8;

used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads

NEWS

added Mirabelle option "-y" for dry run

tuned garbage optimization

added cpu time (in ms) to Mirabelle run_action output

added Mirabelle option -r to randomize the goals before selection

A new lemma about inverse image

proper treatment of $let variables in symbol table in Sledgehammer

removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer

merged

split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"

proper name mangling of "undefined" constants in Sledgehammer

earlier availability of lifting

more correct transfer

merged

proper abstraction of function variables when instantiating induction rules in Sledgehammer

added lemma asympD

added lemma

Some lemmas about continuous functions with integral zero

merged

added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp

removed $ite from E 2.6 in THF format

New and simplified theorems

merged

prefixed all mirabelle_sledgehammer output lines with sledgehammer output

added lemma

Tiny additions inspired by Roth development

allow general command transactions with presentation;

more operations;

clarified signature;

tuned signature;

support Gradle as alternative to Maven (again);

tuned mirabelle command-line help message

updated Mirabelle documentation

proper documentation for induction_rules Sledgehammer option

NEWS

merged

used TH1 for Leo-III in sledgehammer

tuned run_sledgehammer and called it directly from Mirabelle

exported Sledgehammer.launch_prover and use it in Mirabelle

proper filtering inf induction rules in Mirabelle

added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle

tuned ATP to use is_widely_irrelevant_const

added support for initialization messages to Mirabelle

tuned comment

support for JSON:API;

support for Flarum server;

tuned whitespace;

tuned imports;

tuned comments;

clarified author names;

clarified author names;

merged

more accurate names; complete coverage of mail addresses;

more standard author_info;

clarified author info and cluster nodes;