isabelle: Graph

have Sledgehammer honor 'smt_nat_as_int' option
2022-02-22, by blanchet
more handling of Zipperposition definitions in Isar proof construction
2022-02-22, by blanchet
handle Zipperposition definitions in Isar proof construction
2022-02-22, by blanchet
parse Zipperposition definitions
2022-02-22, by blanchet
clarified URL;
2022-02-21, by wenzelm
clarified pdf path;
2022-02-21, by wenzelm
HTTP view of Isabelle PDF documentation;
2022-02-21, by wenzelm
clarified signature;
2022-02-21, by wenzelm
more robust;
2022-02-21, by wenzelm
tuned message;
2022-02-21, by wenzelm
clarified signature: more explicit section structure;
2022-02-21, by wenzelm
clarified signature;
2022-02-21, by wenzelm
clarified signature;
2022-02-21, by wenzelm
tuned signature;
2022-02-21, by wenzelm
tuned;
2022-02-21, by wenzelm
clarified URL (again);
2022-02-21, by wenzelm
more robust toplevel url: allow extra "/";
2022-02-21, by wenzelm
clarified signature;
2022-02-21, by wenzelm
clarified signature;
2022-02-20, by wenzelm
clarified signature;
2022-02-20, by wenzelm
support for PDF.js: platform-independent PDF viewer;
2022-02-20, by wenzelm
more robust mime_type;
2022-02-20, by wenzelm
merged
2022-02-18, by wenzelm
improved support for Java Chromium Embedded Framework (JCEF): works on x86_64-linux and x86_64-windows with jdk-15 (not jdk-17), does not work on arm64 and darwin;
2022-02-18, by wenzelm
one new lemma
2022-02-18, by paulson
clarified options;
2022-02-18, by wenzelm
clarified options;
2022-02-18, by wenzelm
clarified directory;
2022-02-18, by wenzelm
tuned whitespace;
2022-02-18, by wenzelm
prefer strict equality, without implicit type conversion;
2022-02-18, by wenzelm
tuned;
2022-02-18, by wenzelm
auto-update by VSCode;
2022-02-18, by wenzelm
more activationEvents, as proposed by Denis Paluca;
2022-02-18, by wenzelm
tuned message;
2022-02-18, by wenzelm
NEWS;
2022-02-18, by wenzelm
run Isabelle/VSCode using local VSCodium installation;
2022-02-18, by wenzelm
provide macos_exe, based on bin/codium from linux;
2022-02-18, by wenzelm
clarified options;
2022-02-18, by wenzelm
Avoid overaggresive splitting.
2022-02-17, by haftmann
more lemmas for distribution
2022-02-17, by haftmann
Avoid overaggresive simplification.
2022-02-17, by haftmann
merged
2022-02-17, by wenzelm
setup VSCode from VSCodium distribution;
2022-02-17, by wenzelm
more robust package_dir, to increase chances that it works with IntelliJ IDEA;
2022-02-17, by wenzelm
NEWS
2022-02-16, by desharna
Mirabelle now considers goals preceding "unfolding" and "using" commands
2022-02-16, by desharna
merged
2022-02-15, by paulson
an assortment of new or stronger lemmas
2022-02-15, by paulson
obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented;
2022-02-15, by wenzelm
print outcome of Sledgehammer search in panel
2022-02-14, by blanchet
print Sledgehammer error message
2022-02-14, by blanchet
updated documentation to current matter of affairs
2022-02-12, by haftmann
unused;
2022-02-10, by wenzelm
clarified signature;
2022-02-10, by wenzelm
merged
2022-02-10, by desharna
added Isabelle identification to Mirabelle output
2022-02-09, by desharna
uniformized fact selection for ATP and SMT in Sledgehammer
2022-02-09, by desharna
provide cache for slow computations;
2022-02-09, by wenzelm
used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
2022-02-09, by desharna
more operations;
2022-02-09, by wenzelm
more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)
2022-02-09, by blanchet
more robust TSTP proof parsing
2022-02-07, by blanchet
added possibility of extra options to SMT slices
2022-02-07, by blanchet
tuned output syntax: Hoare triples are now blocks
2022-02-04, by nipkow
tuned output syntax: INV and VAR are now blocks
2022-02-03, by nipkow
more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
2022-02-02, by blanchet
enable induction in one of Zipperposition's slices
2022-02-02, by blanchet
made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme
2022-02-01, by blanchet
robustly handle empty proof blocks in Isar proof output
2022-02-01, by blanchet
propagate right result when enough proofs have been found
2022-02-01, by blanchet
correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives
2022-02-01, by blanchet
don't lose error messages
2022-02-01, by blanchet
don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice
2022-02-01, by blanchet
careful with partial applications
2022-02-01, by blanchet
don't perform preplaying steps if preplaying is disabled
2022-02-01, by blanchet
adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs
2022-02-01, by blanchet
tuned punctuation
2022-02-01, by blanchet
handle TPTP '!=' more gracefully in Isar proof reconstruction
2022-02-01, by blanchet
guard against duplicate lines in Zipperposition proofs
2022-02-01, by blanchet
tuning
2022-02-01, by blanchet
tuned NEWS
2022-02-01, by blanchet
compile HOL-TPTP
2022-01-31, by blanchet
compile Metis_Examples
2022-01-31, by blanchet
more NEWS
2022-01-31, by blanchet
compile mirabelle
2022-01-31, by blanchet
tweaked Auto Sledgehammer's behavior and output
2022-01-31, by blanchet
updated NEWS
2022-01-31, by blanchet
removed experimental prover z3_tptp
2022-01-31, by blanchet
print more verbose information
2022-01-31, by blanchet
run all installed provers by default
2022-01-31, by blanchet
update slice options centrally
2022-01-31, by blanchet
further work on new Sledgehammer slicing
2022-01-31, by blanchet
tweaked verbose output
2022-01-31, by blanchet
tweak padding of prover slice schedule to include all provers
2022-01-31, by blanchet
implemented 'max_proofs' mechanism
2022-01-31, by blanchet
document new option 'max_proofs'
2022-01-31, by blanchet
crude implementation of centralized slicing
2022-01-31, by blanchet
removed obscure E option
2022-01-31, by blanchet
take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
2022-01-31, by blanchet
rationalize slicing format
2022-01-31, by blanchet
thread slices through
2022-01-31, by blanchet
simplified 'best_slice' data structure and made minor changes to slices
2022-01-31, by blanchet
changed logic of 'slice' option to 'slices'
2022-01-31, by blanchet
updated documentation of 'slice' (now 'slices') option
2022-01-31, by blanchet
revised Sledgehammer documentation
2022-01-31, by blanchet
rationalized output for forthcoming slicing model
2022-01-31, by blanchet
use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code
2022-01-31, by blanchet
disable slicing within ATP module (in preparation for refactoring)
2022-01-31, by blanchet
disable slicing within SMT (in preparation for factoring it out)
2022-01-31, by blanchet
generalized the 'slice' option towards more flexible slicing
2022-01-31, by blanchet
tuned -- fewer warnings;
2022-01-31, by wenzelm
Added a tiny proof
2022-01-29, by paulson
Deletion of a duplicate proof
2022-01-28, by paulson
useful lemma integral_less
2022-01-27, by paulson
merged
2022-01-27, by desharna
removed unused parameter following f9908452b282
2022-01-26, by desharna
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
2022-01-26, by blanchet
fixed dodgy intro! attributes
2022-01-25, by paulson
merged
2022-01-25, by desharna
optimized facts traversal in TPTP translation
2022-01-22, by desharna
optimized app_op_level selection in TPTP generation
2022-01-22, by desharna
tuned trivial check in mirabelle_sledgehammer
2022-01-22, by desharna
renamed run_action to run in Mirabelle.action record
2022-01-22, by desharna
added spying of fact filtering timing
2022-01-22, by desharna
tuned mirabelle_sledgehammer output
2022-01-22, by desharna
added spying to Sledgehammer
2022-01-21, by desharna
proper fact filter for dummy ATPs
2022-01-21, by desharna
added syping of fact filtering time to sledgehammer
2022-01-21, by desharna
removed unsynchronized references in mirabelle_sledgehammer
2022-01-21, by desharna
tuned mirabelle_sledgehammer to have a single call to Synchronized.change per run
2022-01-21, by desharna
updated to polyml-test-15c840d48c9a; build_history_base_arm
2022-01-24, by wenzelm
some updates and clarification on Assumption.export_term;
2022-01-22, by wenzelm
new theorem has_integral_UN
2022-01-21, by paulson
updated to jdk-17.0.2+8;
2022-01-21, by wenzelm
used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads
2022-01-21, by desharna
NEWS
2022-01-20, by desharna
added Mirabelle option "-y" for dry run
2022-01-20, by desharna
tuned garbage optimization
2022-01-20, by desharna
added cpu time (in ms) to Mirabelle run_action output
2022-01-19, by desharna
added Mirabelle option -r to randomize the goals before selection
2022-01-18, by desharna
A new lemma about inverse image
2022-01-17, by paulson
proper treatment of $let variables in symbol table in Sledgehammer
2022-01-16, by desharna
removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer
2022-01-15, by desharna
merged
2022-01-12, by desharna
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
2022-01-11, by desharna
proper name mangling of "undefined" constants in Sledgehammer
2022-01-11, by desharna
earlier availability of lifting
2022-01-11, by haftmann
more correct transfer
2022-01-11, by haftmann
merged
2022-01-10, by desharna
proper abstraction of function variables when instantiating induction rules in Sledgehammer
2022-01-10, by desharna
added lemma asympD
2022-01-10, by desharna
added lemma
2022-01-10, by nipkow
Some lemmas about continuous functions with integral zero
2022-01-09, by paulson
merged
2022-01-07, by desharna
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
2022-01-06, by desharna
removed $ite from E 2.6 in THF format
2022-01-05, by desharna
New and simplified theorems
2022-01-05, by paulson
merged
2022-01-03, by desharna
prefixed all mirabelle_sledgehammer output lines with sledgehammer output
2022-01-03, by desharna
added lemma
2021-12-29, by nipkow
Tiny additions inspired by Roth development
2021-12-26, by paulson
allow general command transactions with presentation;
2021-12-21, by wenzelm
more operations;
2021-12-21, by wenzelm
clarified signature;
2021-12-21, by wenzelm
tuned signature;
2021-12-21, by wenzelm
support Gradle as alternative to Maven (again);
2021-12-21, by wenzelm
tuned mirabelle command-line help message
2021-12-20, by desharna
updated Mirabelle documentation
2021-12-20, by desharna
proper documentation for induction_rules Sledgehammer option
2021-12-20, by desharna
NEWS
2021-12-19, by desharna
merged
2021-12-19, by desharna
used TH1 for Leo-III in sledgehammer
2021-12-18, by desharna
tuned run_sledgehammer and called it directly from Mirabelle
2021-12-18, by desharna
exported Sledgehammer.launch_prover and use it in Mirabelle
2021-12-18, by desharna
proper filtering inf induction rules in Mirabelle
2021-12-18, by desharna
added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
2021-12-17, by desharna
tuned ATP to use is_widely_irrelevant_const
2021-12-17, by desharna
added support for initialization messages to Mirabelle
2021-12-17, by desharna
tuned comment
2021-12-17, by blanchet
support for JSON:API;
2021-12-15, by wenzelm
support for Flarum server;
2021-12-15, by wenzelm
tuned whitespace;
2021-12-15, by wenzelm
tuned imports;
2021-12-15, by wenzelm
tuned comments;
2021-12-15, by wenzelm
clarified author names;
2021-12-15, by wenzelm
clarified author names;
2021-12-15, by wenzelm
merged
2021-12-14, by wenzelm
more accurate names;
2021-12-14, by wenzelm
more standard author_info;
2021-12-14, by wenzelm
clarified author info and cluster nodes;
2021-12-14, by wenzelm
more data integrity: name vs. address;
2021-12-14, by wenzelm
clarified signature: more operations;
2021-12-14, by wenzelm
clarified signature;
2021-12-14, by wenzelm
tuned;
2021-12-14, by wenzelm
more data integrity: name vs. address;
2021-12-14, by wenzelm
tuned comments;
2021-12-14, by wenzelm
merged
2021-12-14, by desharna
tuned ATP to use fold_index
2021-12-13, by desharna
tuned sledgehammer to use map_index
2021-12-10, by desharna
merged
2021-12-13, by wenzelm
more data integrity: name vs. address;
2021-12-13, by wenzelm
misc tuning and clarification;
2021-12-13, by wenzelm
clarified name;
2021-12-13, by wenzelm
more mailing list content;
2021-12-13, by wenzelm
more mailing list content;
2021-12-13, by wenzelm
updated links;
2021-12-13, by wenzelm
added Apache Commons Lang + Text: not particularly exciting, but provides useful things like org.apache.commons.text.StringEscapeUtils or org.apache.commons.text.diff;
2021-12-11, by wenzelm
tuned ATP to use map_index
2021-12-10, by desharna
removed obsolete RC tags;
2021-12-12, by wenzelm
proper path;
2021-12-12, by wenzelm
merged, resolving conflict in src/Doc/Implementation/Logic.thy;
2021-12-12, by wenzelm
Added tag Isabelle2021-1 for changeset c2a2be496f35
2021-12-12, by wenzelm
tuned; Isabelle2021-1
2021-12-11, by wenzelm
proper ML types (amending 1aa92bc4d356);
2021-12-07, by wenzelm
proper types for Scala.Fun instances (amending 1aa92bc4d356);
2021-12-07, by wenzelm
proper syntax category;
2021-12-07, by wenzelm
provide component naproche-20211211;
2021-12-11, by wenzelm
merged
2021-12-10, by wenzelm
more Mailman archives;
2021-12-10, by wenzelm
more Mailman content;
2021-12-10, by wenzelm
clarified signature;
2021-12-10, by wenzelm
tuned metis to use map_index
2021-12-10, by desharna
merged
2021-12-10, by desharna
fixed HOL-TPTP
2021-12-10, by desharna
tuned vars_of_iterm
2021-12-09, by desharna
fixed TPTP generation of multi-arity expressions
2021-12-07, by desharna
proper handling of Hilbert choice in TFX logics
2021-11-29, by desharna
proper tptp_builtins
2021-11-28, by desharna
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
2021-11-28, by desharna
proper proxy for Hilbert choice in TPTP output
2021-11-21, by desharna
proper polymorphism for TH1 format in Sledgehammer
2021-11-19, by desharna
refactored $ite and $let configuration and added dummy_thf_reduced prover
2021-11-19, by desharna
tuned TPTP file names generated by Sledgehammer
2021-11-17, by desharna
tuned SMT-Lib file names generated by Mirabelle
2021-11-17, by desharna
added support for higher-order SMT proof search in Sledgehammer
2021-11-17, by desharna
separated FOOL from $ite/$let in TPTP output
2021-11-12, by desharna
missing latex font
2021-12-09, by nipkow
Rewrite: added links to docu, made more prominent
2021-12-09, by nipkow
discontinued old-style {* verbatim *} tokens;
2021-12-06, by wenzelm
tuned proof;
2021-12-06, by wenzelm