- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Sep 30 2021
Sep 30 2021
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFPdcdc054af4e8: new entry Logging_Independent_Anonymity.
new entry Logging_Independent_Anonymity
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP6fb608556d0b: metadata for Logging_Independent_Anonymity.
metadata for Logging_Independent_Anonymity
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd278a335ac39: eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib".
eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib"
Sep 29 2021
Sep 29 2021
clarified antiquotations;
clarified antiquotations;
clarified antiquotations;
clarified antiquotations;
desharna committed rISABELLE776b74a99449: tuned TPTP parsing of THF function application.
tuned TPTP parsing of THF function application
clarified examples;
desharna committed rISABELLEc1583aa3d861: updated to Zipperposition 2.1.
updated to Zipperposition 2.1
desharna committed rISABELLEd5e034f2c109: fixed veriT environment variable in sledgehammer's documentation.
fixed veriT environment variable in sledgehammer's documentation
Sep 28 2021
Sep 28 2021
avoid overlapping PIDE markup (amending bb25ea271b15);
makarius committed rISABELLE40804452ab6b: recover some Linux test, using virtual machine node (Ubuntu 20.04, 4 cores, 16….
recover some Linux test, using virtual machine node (Ubuntu 20.04, 4 cores, 16…
clarified antiquotations;
clarified antiquotations;
clarified antiquotations;
clarified antiquotations;
clarified antiquotations;
clarified antiquotations;
clarified message;
clarified positions, notably for ML compiler errors;
tuned antiquotations;
proper default for Sledgehammer GUI panel;
makarius committed rISABELLEe585e5a906ba: more convenient ML arguments: avoid excessive nesting of cartouches;.
more convenient ML arguments: avoid excessive nesting of cartouches;
outer syntax: support for control-cartouche tokens;
desharna committed rISABELLEd8dc8fdc46fc: prefer veriT over Z3 in sledgehammer.
prefer veriT over Z3 in sledgehammer
desharna committed rISABELLE3301c0d8b560: added Zipperposition to sledgehammer's default provers.
added Zipperposition to sledgehammer's default provers
Sep 27 2021
Sep 27 2021
provide zipperposition-2.1 (still unused);
feat(SpecCheck) folder renaming, types for tests
Sep 26 2021
Sep 26 2021
makarius committed rAFP2056abab0dd6: mproper proof command 'guess' moved to separate theory "Pure-ex.Guess"….
mproper proof command 'guess' moved to separate theory "Pure-ex.Guess"…
makarius committed rISABELLEb49bd5d9041f: improper proof command 'guess' moved to separate theory "Pure-ex.Guess";.
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
NOT is part of syntax bundle also
Sep 24 2021
Sep 24 2021
tuned proofs --- avoid 'guess';
florian.haftmann committed rISABELLE690928dd6f8f: apply declarations from interpretations in eigen context also.
apply declarations from interpretations in eigen context also
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP61b65f5bfdbe: ported Design-Theory from AFP 2021 to devel.
ported Design-Theory from AFP 2021 to devel
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd724a03eef28: ported Three-Circles from AFP 2021 to devel.
ported Three-Circles from AFP 2021 to devel
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP6929ff388470: ported Cubic_Quartic_Equations from AFP 2021 to devel.
ported Cubic_Quartic_Equations from AFP 2021 to devel
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP983817c24bc0: merge of AFP 2021.
merge of AFP 2021
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPfbfac64da6d5: move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations….
move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations…
paulson <lp15@cam.ac.uk> committed rAFPc4a4c0f9e4c8: new entry Cubic_Quartic_Equations.
new entry Cubic_Quartic_Equations
paulson <lp15@cam.ac.uk> committed rAFP7e6431c07123: Cubic_Quartic_Equations sitegen.
Cubic_Quartic_Equations sitegen
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP56c3e661569f: sitegen for combinatorial design theory.
sitegen for combinatorial design theory
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP7654a7c1d7af: new entry: Combinatorial Design Theory.
new entry: Combinatorial Design Theory
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP65f00954b8a3: sitegen for Three Circles.
sitegen for Three Circles
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP41bc6e38e99f: new entry: Three Circles.
new entry: Three Circles
makarius committed rISABELLE9e71155e3666: grant access to sun.tools.jconsole, as required for Java 17;.
grant access to sun.tools.jconsole, as required for Java 17;
update to e-2.6, following Martin Desharnais;
Sep 23 2021
Sep 23 2021
desharna committed rISABELLE6ab3116a251a: updated to Metis 2.4 (release 20200713).
updated to Metis 2.4 (release 20200713)
Sep 22 2021
Sep 22 2021
avoid problems with launch4j and jdk-17;
update to jdk-17+35 (LTS);
unused since 398b7bb9ebdd;
desharna committed rISABELLEfb8ce6090437: removed checks for non-commercial usage of Vampire as it is now under BSD….
removed checks for non-commercial usage of Vampire as it is now under BSD…
desharna committed rISABELLE398b7bb9ebdd: used Vampire 4.5.1 in Sledgehammer.
used Vampire 4.5.1 in Sledgehammer
desharna committed rISABELLEd8dbe7525ff1: enabled FOOL for Vampire in Sledgehammer.
enabled FOOL for Vampire in Sledgehammer
makarius updated the post content for Blog Post: ML antiquotations for type constructors and term constants.
Sep 21 2021
Sep 21 2021
clarified antiquotations;
clarified antiquotations;
makarius committed rISABELLE1c2c0380d58b: clarified partial application: immediate check of object-logic, and avoidance….
clarified partial application: immediate check of object-logic, and avoidance…
clarified antiquotations;
clarified modules, according to Isabelle/534b231ce041;
clarified signature, according to Isabelle/d882abae3379;
makarius committed rAFPd12a1ce2753f: bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library..
bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.
ML antiquotations for object-logic judgment;
makarius committed rISABELLEe098fa45bfe0: proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;.
proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;
clarified antiquotations;
more uniform syntax;
makarius committed rISABELLEead56ad40e15: bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library..
bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.
makarius committed rISABELLE7bb0ac635397: permissive identification, e.g. relevant for HOL-SPARK examples running on….
permissive identification, e.g. relevant for HOL-SPARK examples running on…
localized command 'syntax' and 'no_syntax';
clarified signature;
clarified signature;