All Stories
Use Results
Edit Query
Hide Query

makarius committed rISABELLE8d0c2d74ad63: tuned proofs --- eliminated 'guess';.

tuned proofs --- eliminated 'guess';

makarius committed rISABELLEb8a191ce08aa: merged.

merged

makarius committed rISABELLE308e74afab83: tuned proofs;.

tuned proofs;

makarius committed rISABELLE5c452041fe83: clarified antiquotations;.

clarified antiquotations;

desharna committed rISABELLE102b55e81aca: proper firstorderization in Sledgehammer.

proper firstorderization in Sledgehammer

Sep 20 2021, 2:09 PM

Sep 19 2021

makarius committed rISABELLE714e87ce6e9d: clarified signature;.

clarified signature;

makarius committed rISABELLEdd04da556d1a: clarified antiquotations;.

clarified antiquotations;

makarius committed rISABELLE3360ea6b659d: more control symbols;.

more control symbols;

makarius committed rISABELLE54b2e5f771da: clarified signature -- prefer antiquotations (with subtle change of exception….

clarified signature -- prefer antiquotations (with subtle change of exception…

makarius committed rISABELLE0a4e93250e44: support ML antiquotations with fn abstraction;.

support ML antiquotations with fn abstraction;

makarius committed rISABELLE46a0bb3d3a7b: unused;.

unused;

Sep 16 2021

makarius committed rISABELLE30a0f5879d90: clarified operations: follow Isabelle/ML more closely;.

clarified operations: follow Isabelle/ML more closely;

Sep 16 2021, 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.

Sep 16 2021, 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…

Sep 16 2021, 2:19 PM

Sep 15 2021

makarius committed rISABELLE6b998ce1b8cb: obsolete;.

obsolete;

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…

makarius committed rISABELLE7b860fa1140f: tuned;.

tuned;

makarius committed rISABELLE19022ea3f8cc: clarified name and options for old vampire-4.2.2;.

clarified name and options for old vampire-4.2.2;

florian.haftmann committed rAFP33b9d9a97696: explicit predicate for confined bit range avoids cyclic rewriting in presence….

makarius committed rISABELLEd7a62db70a07: clarified signature;.

clarified signature;

Sep 15 2021, 10:57 AM

Sep 13 2021

explicit predicate for confined bit range avoids cyclic rewriting in presence…

Sep 13 2021, 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…

Sep 13 2021, 4:19 PM

makarius committed rISABELLE7466b2a3905a: more latex macros;.

more latex macros;

Sep 13 2021, 1:37 PM

makarius committed rISABELLEa117c076aa22: clarified signature;.

clarified signature;

Sep 13 2021, 1:19 PM

makarius committed rISABELLEde4b3abaf3ca: tuned;.

tuned;

Sep 13 2021, 1:19 PM

Sep 12 2021

makarius committed rAFPa168f8f2bbc3: tuned signature, according to Isabelle/28a582aa25dd;.

tuned signature, according to Isabelle/28a582aa25dd;

Sep 12 2021, 10:59 PM

makarius committed rISABELLE28a582aa25dd: more antiquotations;.

more antiquotations;

makarius committed rISABELLE1466f8a2f6dd: more antiquotations;.

more antiquotations;

makarius committed rISABELLEf7ee629b9beb: more antiquotations;.

more antiquotations;

makarius committed rISABELLEffe269e74bdd: more antiquotations;.

more antiquotations;

makarius committed rISABELLE6bc96f31cafd: more antiquotations;.

more antiquotations;

makarius committed rISABELLE33f13d2d211c: clarified antiquotations;.

clarified antiquotations;

makarius committed rISABELLE16e5870fe21e: more antiquotations;.

more antiquotations;

makarius committed rISABELLE45a77ee63e57: more antiquotations;.

more antiquotations;

makarius committed rISABELLEabc878973216: clarified antiquotation;.

clarified antiquotation;

makarius committed rISABELLEac130a6bd6b2: more antiquotations;.

more antiquotations;

makarius committed rISABELLE9a9326a072bb: more antiquotations;.

more antiquotations;

makarius committed rISABELLEee04dc00bf0a: more antiquotations;.

more antiquotations;

makarius committed rISABELLE54279cfcf037: more antiquotations;.

more antiquotations;

makarius committed rISABELLE39c98371606f: tuned;.

tuned;

makarius committed rISABELLEb2ad24b5a42c: more antiquotations;.

more antiquotations;

makarius committed rISABELLEb83fa8f3a271: ML antiquotations for type constructors and term constants;.

ML antiquotations for type constructors and term constants;

makarius committed rISABELLE8d1e27a23dd1: clarified order of extra TFrees: underlying fast_string_ord coincides with Name..

Sep 10 2021

makarius committed rISABELLE7492cd35782e: tuned;.

tuned;

Sep 10 2021, 11:19 PM

makarius committed rISABELLE1fc263b5aac1: NEWS;.

NEWS;

Sep 10 2021, 11:03 PM

makarius committed rISABELLEf79dfc7656ae: miscellaneous examples and experiments for Isabelle/Pure;.

miscellaneous examples and experiments for Isabelle/Pure;

Sep 10 2021, 10:47 PM

makarius committed rISABELLE641300b56ebe: tuned comments;.

tuned comments;

Sep 10 2021, 9:57 PM

makarius committed rAFPcb975509a607: eliminated Specification.definition', following Isabelle/6876e3d5e362;.

eliminated Specification.definition', following Isabelle/6876e3d5e362;

Sep 10 2021, 9:41 PM

makarius committed rAFP72c37b1f419b: clarified signature: more scalable operations, according to….

clarified signature: more scalable operations, according to…

Sep 10 2021, 9:41 PM

clarified order of extra TFrees: underlying fast_string_ord coincides with Name.

makarius committed rISABELLE019fe8238656: NEWS;.

NEWS;

makarius committed rISABELLE6876e3d5e362: unused;.

unused;

makarius committed rISABELLE7829d6435c60: more scalable operations;.

more scalable operations;

makarius committed rISABELLEc2ee8d993d6a: clarified signature: 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…

makarius committed rISABELLE7466b17b0820: more scalable operations;.

more scalable operations;

makarius committed rISABELLEa123db647573: clarified signature;.

clarified signature;

makarius committed rISABELLE8cff7900871f: tuned;.

tuned;

makarius committed rISABELLE57b323e20763: more scalable operations;.

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

makarius committed rISABELLE36f2c4a5c21b: clarified signature;.

clarified signature;

makarius committed rISABELLE64be5f224462: clarified signature;.

clarified signature;

makarius committed rISABELLE0a4cdf0036a0: more robust: client could have terminated already;.

more robust: client could have terminated already;

makarius committed rISABELLE0f3ca0cd8071: clarified signature;.

clarified signature;

makarius committed rISABELLEf084d599bb44: clarified set of items with order of addition;.

clarified set of items with order of addition;

makarius committed rISABELLEad2899cdd528: clarified modules;.

clarified modules;

makarius committed rISABELLE5c110ac28dcf: tuned whitespace;.

tuned whitespace;

makarius committed rISABELLEd01920a8b082: tuned message;.

tuned message;

makarius committed rISABELLE612b7e0d6721: clarified signature;.

clarified signature;

makarius committed rISABELLE04214caeb9ac: simplified: uniqueness check happens in export_consumer;.

simplified: uniqueness check happens in export_consumer;

makarius committed rISABELLE633fe7390c97: tuned;.

tuned;

makarius committed rAFPa265f0b030f3: clarified signature, according to Isabelle/612b7e0d6721;.

clarified signature, according to Isabelle/612b7e0d6721;

Sep 9 2021, 8:42 PM

Sep 7 2021

makarius committed rAFP0608aee85535: tuned signature, according to Isabelle/839a6e284545;.

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 rISABELLE839a6e284545: tuned signature;.

tuned signature;

makarius committed rISABELLEd28a51dd9da6: export other entities, e.g. relevant for formal document output;.

export other entities, e.g. relevant for formal document output;

makarius committed rISABELLEbb37fb85d82c: pointer_eq_ord: minor performance tuning;.

pointer_eq_ord: minor performance tuning;

makarius committed rISABELLEe942eedd9229: more reactive interrupt;.

more reactive interrupt;

makarius committed rISABELLE6d48d6ba58df: more robust: progress.stopped means that build has failed;.

more robust: progress.stopped means that build has failed;

makarius committed rISABELLEbda7a7b3bd41: more reactive interrupt;.

more reactive interrupt;

makarius committed rISABELLE0ba3952f409a: more robust: retain length of results;.

more robust: retain length of results;

makarius committed rISABELLEe117e0c29204: more reactive interrupt;.

more reactive interrupt;

makarius committed rISABELLE53e1a14e2ef1: tuned signature;.

tuned signature;

makarius committed rISABELLE45dc9de1bd33: tuned signature;.

tuned signature;

makarius committed rISABELLE3300847d75ae: tuned signature;.

tuned signature;

makarius committed rISABELLEe6f1990c4d34: tuned;.

tuned;

sterraf committed rAFPe58cb507f0b7: merged.

merged

Sep 7 2021, 3:51 PM

sterraf added a reverting change for rAFPef19e4e58b8c: synthesized formulas have their variables permuted: rAFPdfc972b8491c: Backed out changeset ef19e4e58b8c.

Sep 7 2021, 3:51 PM

sterraf committed rAFPdfc972b8491c: Backed out changeset ef19e4e58b8c.

Backed out changeset ef19e4e58b8c

Sep 7 2021, 3:51 PM

makarius committed rAFP301f0280d6c6: avoid hardwired document;.

avoid hardwired document;

Sep 7 2021, 11:05 AM

makarius committed rAFP4ed6e19f5983: merged.

merged

makarius committed rAFP9a1fa4cf1287: tuned signature, according to Isabelle/9d9e7ed01dbb;.

tuned signature, according to Isabelle/9d9e7ed01dbb;

makarius committed rAFP723c9dd87715: clarified signature, according to Isabelle/9d9e7ed01dbb;.

clarified signature, according to Isabelle/9d9e7ed01dbb;

makarius committed rAFP33062a15318c: clarified signature, according to Isabelle/9d9e7ed01dbb;.

clarified signature, according to Isabelle/9d9e7ed01dbb;

makarius committed rAFP5a2b8f5e016e: clarified signature, according to Isabelle/9d9e7ed01dbb;.

clarified signature, according to Isabelle/9d9e7ed01dbb;

makarius committed rAFPce490469c76e: simplified, using Isabelle/ML operations;.

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…

makarius committed rAFP9a6a94253c8d: more scalable operations;.

more scalable operations;

makarius committed rAFPaf371b9b111d: tuned whitespace;.

tuned whitespace;