- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Sep 20 2021
Sep 20 2021
desharna committed rISABELLE404ce20efc4c: proper constants in TPTP $let binding.
proper constants in TPTP $let binding
more operations from Isabelle/ML;
tuned proofs --- eliminated 'guess';
clarified antiquotations;
desharna committed rISABELLE102b55e81aca: proper firstorderization in Sledgehammer.
proper firstorderization in Sledgehammer
Sep 19 2021
Sep 19 2021
clarified signature;
clarified antiquotations;
more control symbols;
makarius committed rISABELLE54b2e5f771da: clarified signature -- prefer antiquotations (with subtle change of exception….
clarified signature -- prefer antiquotations (with subtle change of exception…
support ML antiquotations with fn abstraction;
Sep 16 2021
Sep 16 2021
clarified operations: follow Isabelle/ML more closely;
dcjm committed rPOLYMLcf6f86a6874c: Add regression test for print fix for functor argument. (authored by dcjm).
Add regression test for print fix for functor argument.
dcjm committed rPOLYMLbc89845e46c7: Create a print function for a type function (e.g. type t = int*int). This is… (authored by dcjm).
Create a print function for a type function (e.g. type t = int*int). This is…
Sep 15 2021
Sep 15 2021
makarius committed rISABELLEc645d973f881: provide current vampire-4.5.1: presently unused in Sledgehammer, but relevant….
provide current vampire-4.5.1: presently unused in Sledgehammer, but relevant…
clarified name and options for old vampire-4.2.2;
clarified signature;
Sep 13 2021
Sep 13 2021
florian.haftmann committed rAFP33b9d9a97696: explicit predicate for confined bit range avoids cyclic rewriting in presence….
explicit predicate for confined bit range avoids cyclic rewriting in presence…
florian.haftmann committed rISABELLE42523fbf643b: explicit predicate for confined bit range avoids cyclic rewriting in presence….
explicit predicate for confined bit range avoids cyclic rewriting in presence…
clarified signature;
Sep 12 2021
Sep 12 2021
tuned signature, according to Isabelle/28a582aa25dd;
more antiquotations;
more antiquotations;
more antiquotations;
more antiquotations;
more antiquotations;
clarified antiquotations;
more antiquotations;
more antiquotations;
clarified antiquotation;
more antiquotations;
more antiquotations;
more antiquotations;
more antiquotations;
more antiquotations;
makarius committed rISABELLEb83fa8f3a271: ML antiquotations for type constructors and term constants;.
ML antiquotations for type constructors and term constants;
Sep 10 2021
Sep 10 2021
makarius committed rISABELLEf79dfc7656ae: miscellaneous examples and experiments for Isabelle/Pure;.
miscellaneous examples and experiments for Isabelle/Pure;
makarius committed rAFPcb975509a607: eliminated Specification.definition', following Isabelle/6876e3d5e362;.
eliminated Specification.definition', following Isabelle/6876e3d5e362;
clarified signature: more scalable operations, according to…
makarius committed rISABELLE8d1e27a23dd1: clarified order of extra TFrees: underlying fast_string_ord coincides with Name..
clarified order of extra TFrees: underlying fast_string_ord coincides with Name.
more scalable operations;
clarified signature: more scalable operations;
makarius committed rISABELLE42db84eaee2d: clarified order of extra type variables, following names more often than….
clarified order of extra type variables, following names more often than…
more scalable operations;
clarified signature;
more scalable operations;
makarius committed rISABELLEaed955bb4cb1: omit obsolete field "xs": originally from fd0f8fa2b6bd, but later unused;.
omit obsolete field "xs": originally from fd0f8fa2b6bd, but later unused;
Sep 9 2021
Sep 9 2021
clarified signature;
clarified signature;
more robust: client could have terminated already;
clarified signature;
clarified set of items with order of addition;
clarified signature;
simplified: uniqueness check happens in export_consumer;
clarified signature, according to Isabelle/612b7e0d6721;
Sep 7 2021
Sep 7 2021
tuned signature, according to Isabelle/839a6e284545;
makarius committed rISABELLEbe49c660ebbf: more markup, e.g. to locate defining theory node in formal document output;.
more markup, e.g. to locate defining theory node in formal document output;
makarius committed rISABELLEd28a51dd9da6: export other entities, e.g. relevant for formal document output;.
export other entities, e.g. relevant for formal document output;
pointer_eq_ord: minor performance tuning;
more reactive interrupt;
makarius committed rISABELLE6d48d6ba58df: more robust: progress.stopped means that build has failed;.
more robust: progress.stopped means that build has failed;
more reactive interrupt;
more robust: retain length of results;
more reactive interrupt;
sterraf added a reverting change for rAFPef19e4e58b8c: synthesized formulas have their variables permuted: rAFPdfc972b8491c: Backed out changeset ef19e4e58b8c.
sterraf committed rAFPdfc972b8491c: Backed out changeset ef19e4e58b8c.
Backed out changeset ef19e4e58b8c
avoid hardwired document;
tuned signature, according to Isabelle/9d9e7ed01dbb;
clarified signature, according to Isabelle/9d9e7ed01dbb;
clarified signature, according to Isabelle/9d9e7ed01dbb;
clarified signature, according to Isabelle/9d9e7ed01dbb;
simplified, using Isabelle/ML operations;
makarius committed rAFPa815068160f3: adapted to Isabelle/36774e8af3db: cannot rely on order of instantiation for….
adapted to Isabelle/36774e8af3db: cannot rely on order of instantiation for…
more scalable operations;