isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 tip

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
isabelle update_cartouches;
2021-12-06, by wenzelm
more symbolic latex_output via XML (using YXML within text);
2021-12-05, by wenzelm
tuned signature: remove unused;
2021-12-05, by wenzelm
prefer symbolic Latex.environment (typeset in Isabelle/Scala);
2021-12-05, by wenzelm
tuned signature;
2021-12-05, by wenzelm
clarified corner cases of syntax;
2021-12-05, by wenzelm
clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2);
2021-12-05, by wenzelm
a slightly simpler proof
2021-12-04, by paulson
provide component naproche-2d99afe5c349;
2021-12-04, by wenzelm
merged
2021-12-04, by wenzelm
Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2
2021-12-04, by wenzelm
more documentation about Type/Const antiquotations;
2021-12-03, by wenzelm
more documentation about document build options;
2021-12-03, by wenzelm
address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of 41d009462d3c);
2021-12-03, by wenzelm
tuned --- fewer IDE warnings;
2021-12-02, by wenzelm