Page MenuHomeIsabelle/Phabricator
Feed All Stories

Sep 7 2021

makarius committed rISABELLE9d9e7ed01dbb: clarified modules;.
clarified modules;
Sep 7 2021, 10:50 AM
makarius committed rISABELLEcbbd08df65bd: merged.
merged
Sep 7 2021, 10:50 AM
makarius committed rISABELLEea9f2cb22e50: more scalable operations;.
more scalable operations;
Sep 7 2021, 10:50 AM
makarius committed rISABELLEa88fda85bd25: more scalable operations;.
more scalable operations;
Sep 7 2021, 10:50 AM
makarius committed rISABELLE5d2b87226cd1: tuned;.
tuned;
Sep 7 2021, 10:50 AM
makarius committed rISABELLE12dac3698efd: clarified signature;.
clarified signature;
Sep 7 2021, 10:50 AM
makarius committed rISABELLE282cd3aa6cc6: clarified modules;.
clarified modules;
Sep 7 2021, 10:50 AM
makarius committed rISABELLE5e3f4efa87f9: unused;.
unused;
Sep 7 2021, 10:50 AM
makarius committed rISABELLEde383840425f: more scalable operations;.
more scalable operations;
Sep 7 2021, 10:50 AM
makarius committed rISABELLEeb265f54e3ce: more efficient operations: traverse hyps only when required;.
more efficient operations: traverse hyps only when required;
Sep 7 2021, 10:50 AM
makarius committed rISABELLEa810e8f2f2e9: unused;.
unused;
Sep 7 2021, 10:50 AM
makarius committed rISABELLE36774e8af3db: more robust signature: result has no particular order;.
more robust signature: result has no particular order;
Sep 7 2021, 10:50 AM
makarius committed rISABELLE914a214e110e: more scalable operations;.
more scalable operations;
Sep 7 2021, 10:50 AM
makarius committed rISABELLEef74cf118da3: clarified;.
clarified;
Sep 7 2021, 10:50 AM
makarius committed rISABELLEdbaed92fd8af: tuned signature;.
tuned signature;
Sep 7 2021, 10:50 AM
makarius committed rISABELLE4426b52eabb4: more scalable operations;.
more scalable operations;
Sep 7 2021, 10:50 AM
makarius committed rISABELLE9eff7c673b42: more scalable operations;.
more scalable operations;
Sep 7 2021, 10:50 AM
makarius committed rISABELLE4f2bd13edce3: clarified signature;.
clarified signature;
Sep 7 2021, 10:50 AM
makarius committed rISABELLE1091880266e5: clarified signature;.
clarified signature;
Sep 7 2021, 10:50 AM
makarius committed rISABELLEb3c65c984210: tuned signature;.
tuned signature;
Sep 7 2021, 10:50 AM
makarius committed rISABELLE76ac4dbb0a22: more scalable operations;.
more scalable operations;
Sep 7 2021, 10:50 AM
makarius committed rISABELLEd637611b41bd: more scalable operations;.
more scalable operations;
Sep 7 2021, 10:50 AM
makarius committed rISABELLEc22e5bdb207d: more scalable operations;.
more scalable operations;
Sep 7 2021, 10:50 AM
makarius committed rISABELLEfdcc7e8f95ea: more scalable operations;.
more scalable operations;
Sep 7 2021, 10:50 AM

Sep 4 2021

sterraf committed rAFPef19e4e58b8c: synthesized formulas have their variables permuted.
synthesized formulas have their variables permuted
Sep 4 2021, 4:20 PM
sterraf committed rAFPf949f8939459: merged.
merged
Sep 4 2021, 4:20 PM
paulson committed rAFP76b26779f90c: merged.
merged
Sep 4 2021, 12:30 PM
paulson <lp15@cam.ac.uk> committed rAFP4e16e45730a4: fixes for cardinality lemmas.
fixes for cardinality lemmas
Sep 4 2021, 12:30 PM
paulson <lp15@cam.ac.uk> committed rISABELLE38c01d7e9f5b: white space.
white space
Sep 4 2021, 12:22 PM
paulson committed rISABELLE54b753b90b87: merged.
merged
Sep 4 2021, 12:22 PM
paulson <lp15@cam.ac.uk> committed rISABELLE527088d4a89b: strengthened a few lemmas about finite sets and added a code equation for….
strengthened a few lemmas about finite sets and added a code equation for…
Sep 4 2021, 12:22 PM
paulson <lp15@cam.ac.uk> committed rISABELLEe04ec2b9ed97: some fixes connected with card_Diff_singleton.
some fixes connected with card_Diff_singleton
Sep 4 2021, 12:22 PM
makarius committed rAFP34eccbb60a01: proper inst table;.
proper inst table;
Sep 4 2021, 12:44 AM

Sep 3 2021

makarius committed rISABELLEbf595bfbdc98: tuned;.
tuned;
Sep 3 2021, 8:44 PM
makarius committed rISABELLE291e71ed0174: proper inst table;.
proper inst table;
Sep 3 2021, 8:44 PM
makarius committed rISABELLEc49134ee16c1: more scalable data structure (but: rarely used many arguments);.
more scalable data structure (but: rarely used many arguments);
Sep 3 2021, 8:44 PM
makarius committed rISABELLE1d25be2353e1: minor performance tuning: fewer allocations;.
minor performance tuning: fewer allocations;
Sep 3 2021, 8:44 PM

Aug 31 2021

makarius committed rISABELLE8798edfc61ef: tuned;.
tuned;
Aug 31 2021, 2:50 PM

Aug 30 2021

makarius committed rISABELLE736374547a7f: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 30 2021, 10:10 PM
makarius committed rISABELLEa308ed696b58: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 30 2021, 10:10 PM
makarius committed rISABELLEe16ac8907148: tuned signature;.
tuned signature;
Aug 30 2021, 10:10 PM
makarius committed rISABELLE7515abfe18cf: avoid change of existing file, notably rebuild via ghc_stack;.
avoid change of existing file, notably rebuild via ghc_stack;
Aug 30 2021, 10:10 PM

Aug 29 2021

makarius committed rISABELLE12152390db34: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 29 2021, 5:41 PM
makarius committed rISABELLEa1ccecae6a57: clarified process description;.
clarified process description;
Aug 29 2021, 5:41 PM

Aug 28 2021

makarius committed rISABELLE2ee03f7abd8d: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 28 2021, 11:30 PM
makarius committed rISABELLEc14774713d62: clarified signature;.
clarified signature;
Aug 28 2021, 11:30 PM

Aug 27 2021

makarius committed rISABELLE24a2a6ced0ab: more Isabelle/Haskell;.
more Isabelle/Haskell;
Aug 27 2021, 9:56 PM
blanchette committed rISABELLE1a8d8dd77513: made sure lambda-lifting works well with native let binders in Sledgehammer.
made sure lambda-lifting works well with native let binders in Sledgehammer
Aug 27 2021, 8:57 PM
Pasquale Noce <pasquale.noce@hidglobal.com> committed rAFP80d141ead0ab: Graphic rendering of Relational_Method PDF files refined..
Graphic rendering of Relational_Method PDF files refined.
Aug 27 2021, 4:15 PM
blanchette committed rISABELLEadf767b94f77: handle Zipperposition's ResourceOut gracefully.
handle Zipperposition's ResourceOut gracefully
Aug 27 2021, 2:50 PM
blanchette committed rISABELLE9c6159cbf9ee: disabled 'ite' in Zipperposition until we upgrade to a version of Zip that….
disabled 'ite' in Zipperposition until we upgrade to a version of Zip that…
Aug 27 2021, 2:50 PM
Pasquale Noce <pasquale.noce@hidglobal.com> committed rAFP5fa903cd1a85: Entry Relational_Method updated..
Entry Relational_Method updated.
Aug 27 2021, 1:42 PM

Aug 26 2021

makarius committed rISABELLE5f0f0553762f: proper test for type constructor;.
proper test for type constructor;
Aug 26 2021, 11:23 PM
makarius committed rISABELLEc832f35ea571: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 26 2021, 10:41 PM
makarius committed rISABELLE92f08f3d77bd: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 26 2021, 10:16 PM
makarius committed rISABELLEc36b663ef037: tuned;.
tuned;
Aug 26 2021, 4:26 PM
makarius committed rISABELLE10455384a3e5: merged.
merged
Aug 26 2021, 4:26 PM
makarius committed rISABELLE17090e27aae9: more scalable data structure (but: rarely used with > 5 arguments);.
more scalable data structure (but: rarely used with > 5 arguments);
Aug 26 2021, 4:26 PM
kappelmann added a reverting change for rISABELLEd4af818e0880: Backed out changeset fe8d0f4da0e6: rISABELLEbf9871795aeb: Backed out changeset d4af818e0880.
Aug 26 2021, 1:42 PM
kappelmann committed rISABELLEbf9871795aeb: Backed out changeset d4af818e0880.
Backed out changeset d4af818e0880
Aug 26 2021, 1:42 PM
makarius committed rAFP0320f17157ee: more realistic timeout;.
more realistic timeout;
Aug 26 2021, 12:15 PM

Aug 25 2021

makarius committed rISABELLE1f78a40e4399: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 25 2021, 10:41 PM
makarius committed rISABELLEf54b061c2c22: merged.
merged
Aug 25 2021, 10:41 PM
makarius committed rISABELLE6dc7ff326906: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 25 2021, 10:41 PM
makarius committed rISABELLE30e2e44baa57: tuned;.
tuned;
Aug 25 2021, 10:41 PM
makarius committed rISABELLEffe24c7da1c6: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 25 2021, 10:41 PM
nipkow committed rISABELLE852df4f1dbfa: unhide canonical function def examples.
unhide canonical function def examples
Aug 25 2021, 10:10 PM
nipkow committed rISABELLE2b00c267196e: reflect moved theories.
reflect moved theories
Aug 25 2021, 10:10 PM
nipkow committed rISABELLEec947c18e060: merged.
merged
Aug 25 2021, 10:10 PM
nipkow committed rISABELLEd4af818e0880: Backed out changeset fe8d0f4da0e6.
Backed out changeset fe8d0f4da0e6
Aug 25 2021, 10:10 PM
nipkow committed rISABELLE9a1796acd0a4: merged.
merged
Aug 25 2021, 10:10 PM
nipkow added a reverting change for rISABELLEfe8d0f4da0e6: remove SpecCheck; it is now part of the AFP: rISABELLEd4af818e0880: Backed out changeset fe8d0f4da0e6.
Aug 25 2021, 10:10 PM
makarius committed rISABELLEea10e06adede: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 25 2021, 1:50 PM

Aug 24 2021

makarius committed rISABELLE6109a9105a7a: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 24 2021, 8:39 PM
makarius committed rISABELLE2508ea6a9a11: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 24 2021, 8:39 PM
makarius committed rISABELLE92e74f9305a4: more Isabelle/Haskell operations;.
more Isabelle/Haskell operations;
Aug 24 2021, 8:39 PM
makarius committed rISABELLE7652f8d29d10: clarified signature;.
clarified signature;
Aug 24 2021, 3:50 PM
makarius committed rISABELLE72bb7e9143f7: minor performance tuning;.
minor performance tuning;
Aug 24 2021, 3:50 PM
makarius committed rISABELLEaf81e4a307be: clarified signature;.
clarified signature;
Aug 24 2021, 3:50 PM
makarius committed rISABELLE5d40a4f66fdd: tuned;.
tuned;
Aug 24 2021, 3:50 PM
makarius committed rISABELLE4ae14c2e7cdd: tuned;.
tuned;
Aug 24 2021, 3:50 PM
makarius committed rISABELLE5f81ebfb551e: tuned comments;.
tuned comments;
Aug 24 2021, 3:50 PM
makarius committed rISABELLE54e096758b63: tuned signature;.
tuned signature;
Aug 24 2021, 3:50 PM
makarius committed rAFPd5bc84fd503c: clarified signature;.
clarified signature;
Aug 24 2021, 3:50 PM

Aug 23 2021

makarius committed rAFPf1bf23e16821: follow Isabelle/53e28c438f96;.
follow Isabelle/53e28c438f96;
Aug 23 2021, 10:29 PM
makarius committed rISABELLEa8b032dede5c: treat Symbol.eof as in ML (but: presently unused);.
treat Symbol.eof as in ML (but: presently unused);
Aug 23 2021, 10:29 PM
makarius committed rISABELLEb70714530045: tuned;.
tuned;
Aug 23 2021, 10:29 PM
makarius committed rISABELLE53e28c438f96: minor performance tuning;.
minor performance tuning;
Aug 23 2021, 10:29 PM
makarius committed rAFPe3caeb84ccd9: clarified signature, following Isabelle/a3b0fc510705;.
clarified signature, following Isabelle/a3b0fc510705;
Aug 23 2021, 6:40 PM
makarius committed rISABELLE8d03d548df1c: proper Isabelle symbol positions;.
proper Isabelle symbol positions;
Aug 23 2021, 6:38 PM
makarius committed rISABELLEa3b0fc510705: clarified signature;.
clarified signature;
Aug 23 2021, 6:38 PM
makarius committed rISABELLEc576a4e2ffbc: more Haskell operations;.
more Haskell operations;
Aug 23 2021, 6:38 PM
makarius committed rISABELLEa9e79c3645c4: clarified signature;.
clarified signature;
Aug 23 2021, 6:38 PM
makarius committed rISABELLE43fe7388458f: tuned;.
tuned;
Aug 23 2021, 6:38 PM
makarius committed rISABELLE09d4175f473e: tuned;.
tuned;
Aug 23 2021, 6:38 PM

Aug 22 2021

makarius committed rISABELLEf0b2136e2204: tuned signature: prefer existing Haskell operations;.
tuned signature: prefer existing Haskell operations;
Aug 22 2021, 9:59 PM
makarius committed rISABELLE25c672c32467: more Haskell operations;.
more Haskell operations;
Aug 22 2021, 9:55 PM
makarius committed rISABELLE86163ea20e77: tuned comments;.
tuned comments;
Aug 22 2021, 8:17 PM
makarius committed rISABELLEff3dbb2be924: tuned signature;.
tuned signature;
Aug 22 2021, 8:17 PM
nipkow committed rAFP376d3a9f6285: tuned.
tuned
Aug 22 2021, 2:23 PM