| 2021-09-28 |
nipkow |
merged
|
changeset |
files
|
| 2021-09-28 |
nipkow |
An example
|
changeset |
files
|
| 2021-09-28 |
desharna |
prefer veriT over Z3 in sledgehammer
|
changeset |
files
|
| 2021-09-28 |
desharna |
added Zipperposition to sledgehammer's default provers
|
changeset |
files
|
| 2021-09-27 |
wenzelm |
provide zipperposition-2.1 (still unused);
|
changeset |
files
|
| 2021-09-27 |
blanchet |
tuned docs
|
changeset |
files
|
| 2021-09-26 |
wenzelm |
merged
|
changeset |
files
|
| 2021-09-26 |
wenzelm |
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
|
changeset |
files
|
| 2021-09-25 |
haftmann |
NOT is part of syntax bundle also
|
changeset |
files
|
| 2021-09-24 |
wenzelm |
merged
|
changeset |
files
|
| 2021-09-24 |
wenzelm |
tuned proofs --- avoid 'guess';
|
changeset |
files
|
| 2021-09-24 |
haftmann |
apply declarations from interpretations in eigen context also
|
changeset |
files
|
| 2021-09-24 |
wenzelm |
grant access to sun.tools.jconsole, as required for Java 17;
|
changeset |
files
|
| 2021-09-24 |
wenzelm |
update to e-2.6, following Martin Desharnais;
|
changeset |
files
|
| 2021-09-23 |
desharna |
updated to Metis 2.4 (release 20200713)
|
changeset |
files
|
| 2021-09-22 |
wenzelm |
avoid problems with launch4j and jdk-17;
|
changeset |
files
|
| 2021-09-22 |
wenzelm |
update to jdk-17+35 (LTS);
|
changeset |
files
|
| 2021-09-22 |
wenzelm |
tuned message;
|
changeset |
files
|
| 2021-09-22 |
wenzelm |
unused since 398b7bb9ebdd;
|
changeset |
files
|
| 2021-09-22 |
desharna |
merged
|
changeset |
files
|
| 2021-09-22 |
desharna |
removed checks for non-commercial usage of Vampire as it is now under BSD licence
|
changeset |
files
|
| 2021-09-22 |
desharna |
enabled FOOL for Vampire in Sledgehammer
|
changeset |
files
|
| 2021-09-22 |
desharna |
used Vampire 4.5.1 in Sledgehammer
|
changeset |
files
|
| 2021-09-22 |
wenzelm |
proper NEWS;
|
changeset |
files
|
| 2021-09-22 |
wenzelm |
tuned NEWS;
|
changeset |
files
|
| 2021-09-21 |
wenzelm |
clarified antiquotations;
|
changeset |
files
|
| 2021-09-21 |
wenzelm |
clarified antiquotations;
|
changeset |
files
|
| 2021-09-21 |
wenzelm |
clarified antiquotations;
|
changeset |
files
|
| 2021-09-21 |
wenzelm |
clarified partial application: immediate check of object-logic, and avoidance of context within closure;
|
changeset |
files
|
| 2021-09-21 |
wenzelm |
merged
|
changeset |
files
|
| 2021-09-21 |
wenzelm |
clarified antiquotations;
|
changeset |
files
|
| 2021-09-21 |
wenzelm |
ML antiquotations for object-logic judgment;
|
changeset |
files
|
| 2021-09-21 |
wenzelm |
proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;
|
changeset |
files
|
| 2021-09-21 |
wenzelm |
clarified modules;
|
changeset |
files
|
| 2021-09-21 |
wenzelm |
clarified modules;
|
changeset |
files
|
| 2021-09-21 |
wenzelm |
more uniform syntax;
|
changeset |
files
|
| 2021-09-21 |
wenzelm |
permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone;
|
changeset |
files
|
| 2021-09-20 |
wenzelm |
NEWS;
|
changeset |
files
|
| 2021-09-20 |
wenzelm |
bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax;
|
changeset |
files
|
| 2021-09-20 |
wenzelm |
localized command 'syntax' and 'no_syntax';
|
changeset |
files
|
| 2021-09-20 |
wenzelm |
tuned;
|
changeset |
files
|
| 2021-09-20 |
wenzelm |
clarified signature;
|
changeset |
files
|
| 2021-09-20 |
wenzelm |
clarified signature;
|
changeset |
files
|
| 2021-09-20 |
desharna |
merged
|
changeset |
files
|
| 2021-09-20 |
desharna |
proper constants in TPTP $let binding
|
changeset |
files
|
| 2021-09-20 |
wenzelm |
more operations from Isabelle/ML;
|
changeset |
files
|
| 2021-09-20 |
wenzelm |
merged
|
changeset |
files
|
| 2021-09-20 |
wenzelm |
tuned proofs --- eliminated 'guess';
|
changeset |
files
|
| 2021-09-20 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2021-09-20 |
wenzelm |
clarified antiquotations;
|
changeset |
files
|
| 2021-09-20 |
desharna |
proper firstorderization in Sledgehammer
|
changeset |
files
|
| 2021-09-19 |
wenzelm |
clarified signature;
|
changeset |
files
|
| 2021-09-19 |
wenzelm |
clarified antiquotations;
|
changeset |
files
|
| 2021-09-19 |
wenzelm |
clarified signature -- prefer antiquotations (with subtle change of exception content);
|
changeset |
files
|
| 2021-09-19 |
wenzelm |
more control symbols;
|
changeset |
files
|
| 2021-09-19 |
wenzelm |
support ML antiquotations with fn abstraction;
|
changeset |
files
|
| 2021-09-19 |
wenzelm |
unused;
|
changeset |
files
|
| 2021-09-16 |
wenzelm |
clarified operations: follow Isabelle/ML more closely;
|
changeset |
files
|
| 2021-09-15 |
wenzelm |
provide current vampire-4.5.1: presently unused in Sledgehammer, but relevant for Isabelle/Naproche;
|
changeset |
files
|
| 2021-09-15 |
wenzelm |
obsolete;
|
changeset |
files
|