Page MenuHomeIsabelle/Phabricator
Feed All Stories

Yesterday

desharna committed rISABELLE949054d78a77: merged.
merged
Mon, Sep 20, 8:25 PM
desharna committed rISABELLE404ce20efc4c: proper constants in TPTP $let binding.
proper constants in TPTP $let binding
Mon, Sep 20, 8:25 PM
makarius committed rISABELLE9dca3df78b6a: more operations from Isabelle/ML;.
more operations from Isabelle/ML;
Mon, Sep 20, 3:27 PM
makarius committed rISABELLE8d0c2d74ad63: tuned proofs --- eliminated 'guess';.
tuned proofs --- eliminated 'guess';
Mon, Sep 20, 3:27 PM
makarius committed rISABELLEb8a191ce08aa: merged.
merged
Mon, Sep 20, 3:27 PM
makarius committed rISABELLE308e74afab83: tuned proofs;.
tuned proofs;
Mon, Sep 20, 3:27 PM
makarius committed rISABELLE5c452041fe83: clarified antiquotations;.
clarified antiquotations;
Mon, Sep 20, 3:27 PM
desharna committed rISABELLE102b55e81aca: proper firstorderization in Sledgehammer.
proper firstorderization in Sledgehammer
Mon, Sep 20, 2:09 PM

Sun, Sep 19

makarius committed rISABELLE714e87ce6e9d: clarified signature;.
clarified signature;
Sun, Sep 19, 10:02 PM
makarius committed rISABELLEdd04da556d1a: clarified antiquotations;.
clarified antiquotations;
Sun, Sep 19, 10:02 PM
makarius committed rISABELLE3360ea6b659d: more control symbols;.
more control symbols;
Sun, Sep 19, 10:02 PM
makarius committed rISABELLE54b2e5f771da: clarified signature -- prefer antiquotations (with subtle change of exception….
clarified signature -- prefer antiquotations (with subtle change of exception…
Sun, Sep 19, 10:02 PM
makarius committed rISABELLE0a4e93250e44: support ML antiquotations with fn abstraction;.
support ML antiquotations with fn abstraction;
Sun, Sep 19, 10:02 PM
makarius committed rISABELLE46a0bb3d3a7b: unused;.
unused;
Sun, Sep 19, 10:02 PM

Thu, Sep 16

makarius committed rISABELLE30a0f5879d90: clarified operations: follow Isabelle/ML more closely;.
clarified operations: follow Isabelle/ML more closely;
Thu, Sep 16, 7:05 PM
dcjm committed rPOLYMLcf6f86a6874c: Add regression test for print fix for functor argument. (authored by dcjm).
Add regression test for print fix for functor argument.
Thu, Sep 16, 5:17 PM
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…
Thu, Sep 16, 2:19 PM

Wed, Sep 15

makarius committed rISABELLE6b998ce1b8cb: obsolete;.
obsolete;
Wed, Sep 15, 8:09 PM
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…
Wed, Sep 15, 8:09 PM
makarius committed rISABELLE7b860fa1140f: tuned;.
tuned;
Wed, Sep 15, 8:09 PM
makarius committed rISABELLE19022ea3f8cc: clarified name and options for old vampire-4.2.2;.
clarified name and options for old vampire-4.2.2;
Wed, Sep 15, 8:09 PM
makarius committed rISABELLEd7a62db70a07: clarified signature;.
clarified signature;
Wed, Sep 15, 10:57 AM

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…
Mon, Sep 13, 4:20 PM
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…
Mon, Sep 13, 4:19 PM
makarius committed rISABELLE7466b2a3905a: more latex macros;.
more latex macros;
Mon, Sep 13, 1:37 PM
makarius committed rISABELLEa117c076aa22: clarified signature;.
clarified signature;
Mon, Sep 13, 1:19 PM
makarius committed rISABELLEde4b3abaf3ca: tuned;.
tuned;
Mon, Sep 13, 1:19 PM

Sun, Sep 12

makarius committed rAFPa168f8f2bbc3: tuned signature, according to Isabelle/28a582aa25dd;.
tuned signature, according to Isabelle/28a582aa25dd;
Sun, Sep 12, 10:59 PM
makarius committed rISABELLE28a582aa25dd: more antiquotations;.
more antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLE1466f8a2f6dd: more antiquotations;.
more antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLEf7ee629b9beb: more antiquotations;.
more antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLEffe269e74bdd: more antiquotations;.
more antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLE6bc96f31cafd: more antiquotations;.
more antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLE33f13d2d211c: clarified antiquotations;.
clarified antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLE16e5870fe21e: more antiquotations;.
more antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLE45a77ee63e57: more antiquotations;.
more antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLEabc878973216: clarified antiquotation;.
clarified antiquotation;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLEac130a6bd6b2: more antiquotations;.
more antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLE9a9326a072bb: more antiquotations;.
more antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLEee04dc00bf0a: more antiquotations;.
more antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLE54279cfcf037: more antiquotations;.
more antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLE39c98371606f: tuned;.
tuned;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLEb2ad24b5a42c: more antiquotations;.
more antiquotations;
Sun, Sep 12, 10:35 PM
makarius committed rISABELLEb83fa8f3a271: ML antiquotations for type constructors and term constants;.
ML antiquotations for type constructors and term constants;
Sun, Sep 12, 10:35 PM

Fri, Sep 10

makarius committed rISABELLE7492cd35782e: tuned;.
tuned;
Fri, Sep 10, 11:19 PM
makarius committed rISABELLE1fc263b5aac1: NEWS;.
NEWS;
Fri, Sep 10, 11:03 PM
makarius committed rISABELLEf79dfc7656ae: miscellaneous examples and experiments for Isabelle/Pure;.
miscellaneous examples and experiments for Isabelle/Pure;
Fri, Sep 10, 10:47 PM
makarius committed rISABELLE641300b56ebe: tuned comments;.
tuned comments;
Fri, Sep 10, 9:57 PM
makarius committed rAFPcb975509a607: eliminated Specification.definition', following Isabelle/6876e3d5e362;.
eliminated Specification.definition', following Isabelle/6876e3d5e362;
Fri, Sep 10, 9:41 PM
makarius committed rAFP72c37b1f419b: clarified signature: more scalable operations, according to….
clarified signature: more scalable operations, according to…
Fri, Sep 10, 9:41 PM
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.
Fri, Sep 10, 9:39 PM
makarius committed rISABELLE019fe8238656: NEWS;.
NEWS;
Fri, Sep 10, 9:39 PM
makarius committed rISABELLE6876e3d5e362: unused;.
unused;
Fri, Sep 10, 9:39 PM
makarius committed rISABELLE7829d6435c60: more scalable operations;.
more scalable operations;
Fri, Sep 10, 9:39 PM
makarius committed rISABELLEc2ee8d993d6a: clarified signature: more scalable operations;.
clarified signature: more scalable operations;
Fri, Sep 10, 9:39 PM
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…
Fri, Sep 10, 9:39 PM
makarius committed rISABELLE7466b17b0820: more scalable operations;.
more scalable operations;
Fri, Sep 10, 9:39 PM
makarius committed rISABELLEa123db647573: clarified signature;.
clarified signature;
Fri, Sep 10, 9:39 PM
makarius committed rISABELLE8cff7900871f: tuned;.
tuned;
Fri, Sep 10, 9:39 PM
makarius committed rISABELLE57b323e20763: more scalable operations;.
more scalable operations;
Fri, Sep 10, 9:39 PM
makarius committed rISABELLEaed955bb4cb1: omit obsolete field "xs": originally from fd0f8fa2b6bd, but later unused;.
omit obsolete field "xs": originally from fd0f8fa2b6bd, but later unused;
Fri, Sep 10, 9:39 PM

Thu, Sep 9

makarius committed rISABELLE36f2c4a5c21b: clarified signature;.
clarified signature;
Thu, Sep 9, 8:44 PM
makarius committed rISABELLE64be5f224462: clarified signature;.
clarified signature;
Thu, Sep 9, 8:44 PM
makarius committed rISABELLE0a4cdf0036a0: more robust: client could have terminated already;.
more robust: client could have terminated already;
Thu, Sep 9, 8:44 PM
makarius committed rISABELLE0f3ca0cd8071: clarified signature;.
clarified signature;
Thu, Sep 9, 8:44 PM
makarius committed rISABELLEf084d599bb44: clarified set of items with order of addition;.
clarified set of items with order of addition;
Thu, Sep 9, 8:44 PM
makarius committed rISABELLEad2899cdd528: clarified modules;.
clarified modules;
Thu, Sep 9, 8:44 PM
makarius committed rISABELLE5c110ac28dcf: tuned whitespace;.
tuned whitespace;
Thu, Sep 9, 8:44 PM
makarius committed rISABELLEd01920a8b082: tuned message;.
tuned message;
Thu, Sep 9, 8:44 PM
makarius committed rISABELLE612b7e0d6721: clarified signature;.
clarified signature;
Thu, Sep 9, 8:44 PM
makarius committed rISABELLE04214caeb9ac: simplified: uniqueness check happens in export_consumer;.
simplified: uniqueness check happens in export_consumer;
Thu, Sep 9, 8:44 PM
makarius committed rISABELLE633fe7390c97: tuned;.
tuned;
Thu, Sep 9, 8:44 PM
makarius committed rAFPa265f0b030f3: clarified signature, according to Isabelle/612b7e0d6721;.
clarified signature, according to Isabelle/612b7e0d6721;
Thu, Sep 9, 8:42 PM

Tue, Sep 7

makarius committed rAFP0608aee85535: tuned signature, according to Isabelle/839a6e284545;.
tuned signature, according to Isabelle/839a6e284545;
Tue, Sep 7, 11:09 PM
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;
Tue, Sep 7, 11:09 PM
makarius committed rISABELLE839a6e284545: tuned signature;.
tuned signature;
Tue, Sep 7, 11:09 PM
makarius committed rISABELLEd28a51dd9da6: export other entities, e.g. relevant for formal document output;.
export other entities, e.g. relevant for formal document output;
Tue, Sep 7, 11:09 PM
makarius committed rISABELLEbb37fb85d82c: pointer_eq_ord: minor performance tuning;.
pointer_eq_ord: minor performance tuning;
Tue, Sep 7, 11:09 PM
makarius committed rISABELLEe942eedd9229: more reactive interrupt;.
more reactive interrupt;
Tue, Sep 7, 11:09 PM
makarius committed rISABELLE6d48d6ba58df: more robust: progress.stopped means that build has failed;.
more robust: progress.stopped means that build has failed;
Tue, Sep 7, 11:09 PM
makarius committed rISABELLEbda7a7b3bd41: more reactive interrupt;.
more reactive interrupt;
Tue, Sep 7, 11:09 PM
makarius committed rISABELLE0ba3952f409a: more robust: retain length of results;.
more robust: retain length of results;
Tue, Sep 7, 11:09 PM
makarius committed rISABELLEe117e0c29204: more reactive interrupt;.
more reactive interrupt;
Tue, Sep 7, 11:09 PM
makarius committed rISABELLE53e1a14e2ef1: tuned signature;.
tuned signature;
Tue, Sep 7, 11:09 PM
makarius committed rISABELLE45dc9de1bd33: tuned signature;.
tuned signature;
Tue, Sep 7, 11:09 PM
makarius committed rISABELLE3300847d75ae: tuned signature;.
tuned signature;
Tue, Sep 7, 11:09 PM
makarius committed rISABELLEe6f1990c4d34: tuned;.
tuned;
Tue, Sep 7, 11:09 PM
sterraf committed rAFPe58cb507f0b7: merged.
merged
Tue, Sep 7, 3:51 PM
sterraf added a reverting change for rAFPef19e4e58b8c: synthesized formulas have their variables permuted: rAFPdfc972b8491c: Backed out changeset ef19e4e58b8c.
Tue, Sep 7, 3:51 PM
sterraf committed rAFPdfc972b8491c: Backed out changeset ef19e4e58b8c.
Backed out changeset ef19e4e58b8c
Tue, Sep 7, 3:51 PM
makarius committed rAFP301f0280d6c6: avoid hardwired document;.
avoid hardwired document;
Tue, Sep 7, 11:05 AM
makarius committed rAFP4ed6e19f5983: merged.
merged
Tue, Sep 7, 10:51 AM
makarius committed rAFP9a1fa4cf1287: tuned signature, according to Isabelle/9d9e7ed01dbb;.
tuned signature, according to Isabelle/9d9e7ed01dbb;
Tue, Sep 7, 10:51 AM
makarius committed rAFP723c9dd87715: clarified signature, according to Isabelle/9d9e7ed01dbb;.
clarified signature, according to Isabelle/9d9e7ed01dbb;
Tue, Sep 7, 10:51 AM
makarius committed rAFP33062a15318c: clarified signature, according to Isabelle/9d9e7ed01dbb;.
clarified signature, according to Isabelle/9d9e7ed01dbb;
Tue, Sep 7, 10:51 AM
makarius committed rAFP5a2b8f5e016e: clarified signature, according to Isabelle/9d9e7ed01dbb;.
clarified signature, according to Isabelle/9d9e7ed01dbb;
Tue, Sep 7, 10:51 AM
makarius committed rAFPce490469c76e: simplified, using Isabelle/ML operations;.
simplified, using Isabelle/ML operations;
Tue, Sep 7, 10:51 AM
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…
Tue, Sep 7, 10:51 AM
makarius committed rAFP9a6a94253c8d: more scalable operations;.
more scalable operations;
Tue, Sep 7, 10:51 AM
makarius committed rAFPaf371b9b111d: tuned whitespace;.
tuned whitespace;
Tue, Sep 7, 10:51 AM