2021-12-07 |
desharna |
fixed TPTP generation of multi-arity expressions
|
changeset |
files
|
2021-11-29 |
desharna |
proper handling of Hilbert choice in TFX logics
|
changeset |
files
|
2021-11-28 |
desharna |
proper tptp_builtins
|
changeset |
files
|
2021-11-28 |
desharna |
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
|
changeset |
files
|
2021-11-21 |
desharna |
proper proxy for Hilbert choice in TPTP output
|
changeset |
files
|
2021-11-19 |
desharna |
proper polymorphism for TH1 format in Sledgehammer
|
changeset |
files
|
2021-11-19 |
desharna |
refactored $ite and $let configuration and added dummy_thf_reduced prover
|
changeset |
files
|
2021-11-17 |
desharna |
tuned TPTP file names generated by Sledgehammer
|
changeset |
files
|
2021-11-17 |
desharna |
tuned SMT-Lib file names generated by Mirabelle
|
changeset |
files
|
2021-11-17 |
desharna |
added support for higher-order SMT proof search in Sledgehammer
|
changeset |
files
|
2021-11-11 |
desharna |
separated FOOL from $ite/$let in TPTP output
|
changeset |
files
|
2021-12-09 |
nipkow |
missing latex font
|
changeset |
files
|
2021-12-09 |
nipkow |
Rewrite: added links to docu, made more prominent
|
changeset |
files
|
2021-12-06 |
wenzelm |
discontinued old-style {* verbatim *} tokens;
|
changeset |
files
|
2021-12-06 |
wenzelm |
tuned proof;
|
changeset |
files
|
2021-12-06 |
wenzelm |
isabelle update_cartouches;
|
changeset |
files
|
2021-12-05 |
wenzelm |
more symbolic latex_output via XML (using YXML within text);
|
changeset |
files
|
2021-12-05 |
wenzelm |
tuned signature: remove unused;
|
changeset |
files
|
2021-12-05 |
wenzelm |
prefer symbolic Latex.environment (typeset in Isabelle/Scala);
|
changeset |
files
|
2021-12-05 |
wenzelm |
tuned signature;
|
changeset |
files
|
2021-12-05 |
wenzelm |
clarified corner cases of syntax;
|
changeset |
files
|
2021-12-05 |
wenzelm |
clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2);
|
changeset |
files
|
2021-12-04 |
paulson |
a slightly simpler proof
|
changeset |
files
|
2021-12-04 |
wenzelm |
provide component naproche-2d99afe5c349;
|
changeset |
files
|
2021-12-04 |
wenzelm |
merged
|
changeset |
files
|
2021-12-04 |
wenzelm |
Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2
|
changeset |
files
|
2021-12-03 |
wenzelm |
more documentation about Type/Const antiquotations;
|
changeset |
files
|
2021-12-03 |
wenzelm |
more documentation about document build options;
|
changeset |
files
|
2021-12-03 |
wenzelm |
address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of 41d009462d3c);
|
changeset |
files
|
2021-12-02 |
wenzelm |
tuned --- fewer IDE warnings;
|
changeset |
files
|
2021-11-30 |
wenzelm |
more robust physical timeout (despite 1bea05713dde), especially relevant for quickcheck where large unary numerals may cause excessive heap allocations and resulting GC is better included in the timing;
|
changeset |
files
|
2021-11-28 |
desharna |
added definitions multp{DM,HO} and corresponding lemmas
|
changeset |
files
|
2021-11-28 |
desharna |
added wfP_less to wellorder and wfP_less_multiset
|
changeset |
files
|
2021-11-28 |
desharna |
restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3
|
changeset |
files
|
2021-11-27 |
desharna |
merged
|
changeset |
files
|
2021-11-27 |
desharna |
added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to Multiset
|
changeset |
files
|
2021-11-27 |
desharna |
redefined less_multiset to be based on multp
|
changeset |
files
|
2021-11-27 |
desharna |
added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp
|
changeset |
files
|
2021-11-27 |
desharna |
added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max
|
changeset |
files
|
2021-11-27 |
desharna |
added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp
|
changeset |
files
|
2021-11-27 |
desharna |
added lemma wfP_multp
|
changeset |
files
|
2021-11-27 |
desharna |
added lemma mono_multp
|
changeset |
files
|
2021-11-26 |
desharna |
added Multiset.multp as predicate equivalent of Multiset.mult
|
changeset |
files
|
2021-11-27 |
wenzelm |
address problems with launch4j and jdk-17 (see also 41d009462d3c);
|
changeset |
files
|
2021-11-27 |
wenzelm |
more robust build on midrange hardware;
|
changeset |
files
|
2021-11-27 |
wenzelm |
clarified tests: omit somewhat pointless (unstable) results;
|
changeset |
files
|
2021-11-27 |
wenzelm |
proper fields for gnuplot (amending b614e3e4146a);
|
changeset |
files
|
2021-11-27 |
wenzelm |
tuned output;
|
changeset |
files
|
2021-11-27 |
wenzelm |
tuned;
|
changeset |
files
|
2021-11-26 |
wenzelm |
merged
|
changeset |
files
|
2021-11-26 |
wenzelm |
more robust build on midrange hardware (despite 67d6f1708ea4);
|
changeset |
files
|
2021-11-26 |
wenzelm |
Added tag Isabelle2021-1-RC4 for changeset 2336356d4180
|
changeset |
files
|
2021-11-26 |
wenzelm |
updated to polyml-5.9;
|
changeset |
files
|
2021-11-26 |
wenzelm |
NEWS on "isabelle mirabelle";
|
changeset |
files
|
2021-11-26 |
wenzelm |
tuned;
|
changeset |
files
|
2021-11-25 |
wenzelm |
clarified default for kodkod_scala;
|
changeset |
files
|
2021-11-25 |
wenzelm |
maintain option kodkod_scala within theory context, to allow local modification;
|
changeset |
files
|
2021-11-25 |
wenzelm |
NEWS for proper release;
|
changeset |
files
|
2021-11-25 |
wenzelm |
updated to flatlaf-1.6.4;
|
changeset |
files
|
2021-11-25 |
wenzelm |
avoid broken links: auxiliary files are not yet supported;
|
changeset |
files
|