- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs

Feed All Stories

# All Stories

All Stories

# Yesterday

Yesterday

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

# Sun, Sep 19

Sun, Sep 19

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;

# Thu, Sep 16

Thu, Sep 16

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…

# Wed, Sep 15

Wed, Sep 15

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;

# Mon, Sep 13

Mon, Sep 13

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;

# Sun, Sep 12

Sun, Sep 12

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;

# Fri, Sep 10

Fri, Sep 10

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;

# Thu, Sep 9

Thu, Sep 9

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;

# Tue, Sep 7

Tue, Sep 7

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;