Page MenuHomeIsabelle/Phabricator
Feed All Transactions
AuthorObjectTransactionDate
florian.haftmannrISABELLE5689f0db4508: more simp rules for concrete numerical valuesJul 12 2020, 8:10 PM
makariusrAFP1bb7b24f2cf5: more realistic timeout: 20min CPU time;Jul 11 2020, 10:25 PM
makariusrAFPaeedb987222c: tuned whitespace;Jul 11 2020, 10:21 PM
florian.haftmannrISABELLE9b4135e8bade: a generic horner sum operationJul 11 2020, 8:09 PM
florian.haftmannrISABELLE08348e364739: more thmsJul 11 2020, 8:09 PM
makariusrISABELLE940195fbb282: clarified messages;Jul 11 2020, 6:21 PM
makariusrISABELLE45865bb06182: clarified message --- as in former ML version (see 940195fbb282);Jul 11 2020, 6:21 PM
makariusrISABELLE45865bb06182: clarified message --- as in former ML version (see 940195fbb282);Jul 11 2020, 6:19 PM
makariusrISABELLE5469bacf5573: avoid duplicate Timing messages (see also 5c4800f6b25a);Jul 11 2020, 6:17 PM
makariusrISABELLE5c4800f6b25a: more robust protocol for "Timing ..." messages, notably for pide_session=true;Jul 11 2020, 6:17 PM
makariusrISABELLE664e90313a54: clarified signature;Jul 11 2020, 5:15 PM
makariusrISABELLEca69be5f60fe: clarified messages: avoid duplicate Timing;Jul 11 2020, 5:08 PM
makariusrISABELLE940195fbb282: clarified messages;Jul 11 2020, 4:58 PM
makariusrISABELLE5c9984820caa: clarified signature;Jul 11 2020, 4:41 PM
makariusrISABELLE17a41deb5950: tuned;Jul 11 2020, 4:37 PM
makariusrISABELLE5469bacf5573: avoid duplicate Timing messages (see also 5c4800f6b25a);Jul 11 2020, 4:32 PM
makariusrISABELLE6c6609fd898c: more accurate message;Jul 11 2020, 4:25 PM
makariusrISABELLE2550bac18b49: tuned;Jul 11 2020, 3:52 PM
makariusrISABELLE6a24ecc4ff1b: clarified signature;Jul 11 2020, 3:51 PM
makariusrISABELLEc81e58a81b8c: clarified inlined protocol messages;Jul 11 2020, 3:23 PM
makariusrISABELLE0b1c830ebf3a: removed unused property;Jul 11 2020, 2:44 PM
florian.haftmannrAFP70ae335403b7: signed_take_bitJul 11 2020, 8:21 AM
florian.haftmannrISABELLEa851ce626b78: signed_take_bitJul 11 2020, 8:21 AM
florian.haftmannrISABELLEfebdd4eead56: more on single-bit operationsJul 11 2020, 8:21 AM
"Eugene W. Stark <stark@cs.stonybrook.edu>"rAFP06640f317a79: Add new material, mostly centered around cartesian categories. Sync with my…Jul 10 2020, 11:17 PM
makariusrISABELLE7a53fc156c2b: proper session Timing for build_history log file (see 5c4800f6b25a);Jul 10 2020, 10:46 PM
makariusrISABELLE5c4800f6b25a: more robust protocol for "Timing ..." messages, notably for pide_session=true;Jul 10 2020, 10:46 PM
makariusrISABELLE7a53fc156c2b: proper session Timing for build_history log file (see 5c4800f6b25a);Jul 10 2020, 10:38 PM
makariusrISABELLE13890356df78: clarified signature;Jul 10 2020, 9:58 PM
makariusrISABELLE751f371d6883: more robust, notably for isabelle_cronjob;Jul 10 2020, 9:30 PM
makariusrISABELLE11c46b8e91c0: more robust build_session protocol: allow prover process to terminate/crash…Jul 10 2020, 9:23 PM
desharnarAFPd04de3d51efb: Fix failing proofs after update to Metis 2.4Jul 9 2020, 11:41 AM
desharnarISABELLE913162a47d9f: Update Metis to 2.4Jul 9 2020, 11:39 AM
makariusrISABELLEa7e6ac2dfa58: updated to polyml-5.8.1-20200708: recent repository version for testing;Jul 8 2020, 4:35 PM
makariusrISABELLE5c4800f6b25a: more robust protocol for "Timing ..." messages, notably for pide_session=true;Jul 8 2020, 2:43 PM
dcjmrPOLYML196ac3bc7d11: Move the test for the result of PolyCompareArbitrary up to the top-level of…Jul 7 2020, 9:23 AM
dcjmrPOLYMLf186be011f67: Add PointerEq as a binary operation and reserve WordComparison for the tagged…Jul 6 2020, 6:23 PM
blanchetterISABELLE3e08311ada8e: removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible…Jul 6 2020, 4:52 PM
dcjmrPOLYMLfb10196d998b: Convert single bindings from mutual recursion into simple bindings.Jul 6 2020, 3:26 PM
dcjmrPOLYMLfb10196d998b: Convert single bindings from mutual recursion into simple bindings.Jul 6 2020, 3:26 PM
dcjmrPOLYML19d82db2c17d: Separate out the strongly-connected sets code from CODETREE_FUNCTIONS so it can…Jul 6 2020, 3:26 PM
dcjmrPOLYML744d14ffd49b: Fix bug found by Makarius in generated code. It seems to have been introduced…Jul 6 2020, 3:26 PM
dcjmrPOLYMLfb10196d998b: Convert single bindings from mutual recursion into simple bindings.Jul 6 2020, 2:40 PM
dcjmrPOLYMLa020d4b5f62b: The "setter" for a container refers to the container itself so any bindings…Jul 6 2020, 2:34 PM
florian.haftmannrAFP1cdcce397e9d: separation of traditional bit operationsJul 6 2020, 12:47 PM
florian.haftmannrISABELLE379d0c207c29: separation of traditional bit operationsJul 6 2020, 12:47 PM
dcjmrPOLYMLade5d57318f0: Fix function name: they're mutual bindings not mutable.Jul 6 2020, 9:40 AM
dcjmrPOLYMLd761f194071f: When analysing the usage pattern of a recursive function we need to consider…Jul 6 2020, 9:30 AM
makariusrISABELLE720b72513ae5: no pide_session on macos: avoid odd "hang" of remote_build_history;Jul 5 2020, 11:06 AM
makariusrISABELLEf43b08980f56: support generated preferences, i.e. non-strict system options;Jul 5 2020, 11:00 AM
florian.haftmannrAFPa03e9b5d8dc9: factored out auxiliary theoryJul 4 2020, 10:45 PM
florian.haftmannrISABELLE4a013c92a091: factored out auxiliary theoryJul 4 2020, 10:45 PM
florian.haftmannrISABELLEc7ac6d4f3914: prefer explicit proofJul 4 2020, 10:45 PM
Andreas LochbihlerrAFPb5b8255ae4c4: more operations for maps
Andreas Lochbihler committed rAFPb5b8255ae4c4: more operations for maps. 
Jul 4 2020, 4:25 PM
makariusrISABELLEcb7ddc321f52: tuned whitespace;Jul 3 2020, 5:11 PM
makariusrISABELLEbbec0acf2592: use less memory on old hardware;Jul 3 2020, 5:11 PM
makariusrISABELLE088e3aa85250: clarified signature;Jul 3 2020, 5:00 PM
makariusrISABELLEc8c3f4f0f68b: clarified log message (more uniform);Jul 3 2020, 4:48 PM
florian.haftmannrAFPf90f9d593a88: misc lemma tuningJul 3 2020, 10:01 AM
dcjmrPOLYML7edf731ebd7f: Fix use of "print" rather than "stream" for debugging.Jul 3 2020, 9:36 AM
florian.haftmannrISABELLE8bff286878bf: misc lemma tuningJul 3 2020, 8:18 AM
florian.haftmannrISABELLE66beb9d92e43: explicit proofs for bit projectionsJul 3 2020, 8:18 AM
florian.haftmannrAFPe0714a129570: updated documentationJul 2 2020, 4:27 PM
florian.haftmannrISABELLEbad75618fb82: extraction of equations x = t from premises beneath meta-allJul 2 2020, 2:10 PM
florian.haftmannrAFP81a8bf702c09: activated simproc defined_allJul 2 2020, 2:10 PM
florian.haftmannrISABELLEace45a11a45e: a small aggiornamento for Z2Jul 2 2020, 10:49 AM
florian.haftmannrISABELLEec17263ec38d: removed superfluous dependencyJul 2 2020, 10:49 AM
florian.haftmannrAFPb8a6808299e5: obsolete duplicatesJul 2 2020, 10:41 AM
makariusrISABELLE694009ed4ee1: clarified options --- potentially more robust;Jul 1 2020, 10:11 PM
makariusrISABELLEcea6087e8a70: tuned message;Jul 1 2020, 9:14 PM
florian.haftmannrISABELLEa1cf296a7786: moved to Word_LibJul 1 2020, 7:32 PM
florian.haftmannrAFP3ceb3fe8ab08: factored out ancient numeral representationJul 1 2020, 7:32 PM
florian.haftmannrAFP04f54c116f30: tuned whitespaceJul 1 2020, 7:32 PM
florian.haftmannrAFP82e10d1ca9e1: moved to Word_LibJul 1 2020, 7:32 PM
florian.haftmannrISABELLE76193dd4aec8: factored out ancient numeral representationJul 1 2020, 7:32 PM
florian.haftmannrISABELLE10a8d943a8d8: more explicit proofsJul 1 2020, 7:32 PM
kleingrAFPec1d5c638a9d: merge from afp-2020Jul 1 2020, 4:01 AM
kleingrAFPe4d6b7cae35c: Update history commit links to HeptapodJul 1 2020, 3:31 AM
kleingrAFP4d18e0481131: merge from afp-2020Jul 1 2020, 3:10 AM
kleingrAFPb29dde548f6b: Error message updateJul 1 2020, 3:02 AM
kleingrAFPc6e3efe2d729: One more instance of Bitbucket in READMEJul 1 2020, 3:01 AM
kleingrAFPd3f602e38421: remove Bitbucket from websiteJul 1 2020, 2:59 AM
kleingrAFP331165f0b57c: Update editor instructions for Heptapod + clarificationsJul 1 2020, 2:43 AM
kleingrAFP0519b84e33aa: Convert maintenance instructions to HeptapodJul 1 2020, 2:37 AM
kleingrAFPd78aafccfd60: Update README to HeptapodJul 1 2020, 2:33 AM
kleingrAFP9dfda1e96dc6: Point publish script to heptapodJul 1 2020, 2:33 AM
Julian Brunner <julianbrunner@gmail.com>rAFPca5b629f4e0a: merged
Julian Brunner <julianbrunner@gmail.com> committed rAFPca5b629f4e0a: merged. 
Jun 29 2020, 2:42 PM
kleingrAFP87644ed179f4: Further Bitbucket -> Heptapod docs updateJun 29 2020, 2:38 PM
Julian Brunner <julianbrunner@gmail.com>rAFPf95fe1ab8980: refactoring
Julian Brunner <julianbrunner@gmail.com> committed rAFPf95fe1ab8980: refactoring. 
Jun 29 2020, 10:33 AM
Lars Hupel <lars.hupel@mytum.de>rAFP2f442131b76e: exclude another session on Mac
Lars Hupel <lars.hupel@mytum.de> committed rAFP2f442131b76e: exclude another session on Mac. 
Jun 29 2020, 9:24 AM
kleingrAFP3b5ff4b8d37d: Closing branch "devel"Jun 29 2020, 6:07 AM
kleingrAFPa35807f8a56e: mergeJun 29 2020, 6:04 AM
kleingrAFPc0032d11a990: Bitbucket -> HeptapodJun 29 2020, 4:45 AM
kleingrAFP238b15a87fd2: Update README for HeptapodJun 29 2020, 2:40 AM
GitHub <noreply@github.com>rPOLYMLef44a8b94c08: Merge pull request #135 from pclayton/fix-largeword-fromint
GitHub <noreply@github.com> committed rPOLYMLef44a8b94c08: Merge pull request #135 from pclayton/fix-largeword-fromint (authored by dcjm). 
Jun 28 2020, 3:35 PM
GitHub <noreply@github.com>rPOLYML13efa88e9a1f: Merge pull request #122 from jrtc27/libffi-i386
GitHub <noreply@github.com> committed rPOLYML13efa88e9a1f: Merge pull request #122 from jrtc27/libffi-i386 (authored by dcjm). 
Jun 28 2020, 2:57 PM
makariusrISABELLE0be06f99b210: clarified signature;Jun 27 2020, 11:25 AM
makariusrISABELLE6441b4591eb8: more CONTRIBUTORS;Jun 26 2020, 5:34 PM
makariusrWEBSITE372d301ab6b6: updated URL (auto-forwarded);Jun 26 2020, 5:02 PM
makariusT12: Hosting of Isabelle/AFP after Jun-2020
makarius closed this task as Resolved. 
Jun 26 2020, 4:39 PM