isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -56 +56 +100 +300 +1000 +3000 tip

isabelle