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;

more data integrity: name vs. address;

clarified signature: more operations;

clarified signature;

tuned;

more data integrity: name vs. address;

tuned comments;

merged

tuned ATP to use fold_index

tuned sledgehammer to use map_index

merged

more data integrity: name vs. address;

misc tuning and clarification;

clarified name;

more mailing list content;

more mailing list content;

updated links;

added Apache Commons Lang + Text: not particularly exciting, but provides useful things like org.apache.commons.text.StringEscapeUtils or org.apache.commons.text.diff;

tuned ATP to use map_index

removed obsolete RC tags;

proper path;

merged, resolving conflict in src/Doc/Implementation/Logic.thy;

Added tag Isabelle2021-1 for changeset c2a2be496f35

tuned;