Author | Object | Transaction | Date |
---|
florian.haftmann | rISABELLE5689f0db4508: more simp rules for concrete numerical values | | Jul 12 2020, 8:10 PM |
makarius | rAFP1bb7b24f2cf5: more realistic timeout: 20min CPU time; | | Jul 11 2020, 10:25 PM |
makarius | rAFPaeedb987222c: tuned whitespace; | | Jul 11 2020, 10:21 PM |
florian.haftmann | rISABELLE9b4135e8bade: a generic horner sum operation | | Jul 11 2020, 8:09 PM |
florian.haftmann | rISABELLE08348e364739: more thms | | Jul 11 2020, 8:09 PM |
makarius | rISABELLE940195fbb282: clarified messages; | | Jul 11 2020, 6:21 PM |
makarius | rISABELLE45865bb06182: clarified message --- as in former ML version (see 940195fbb282); | | Jul 11 2020, 6:21 PM |
makarius | rISABELLE45865bb06182: clarified message --- as in former ML version (see 940195fbb282); | | Jul 11 2020, 6:19 PM |
makarius | rISABELLE5469bacf5573: avoid duplicate Timing messages (see also 5c4800f6b25a); | | Jul 11 2020, 6:17 PM |
makarius | rISABELLE5c4800f6b25a: more robust protocol for "Timing ..." messages, notably for pide_session=true; | | Jul 11 2020, 6:17 PM |
makarius | rISABELLE664e90313a54: clarified signature; | | Jul 11 2020, 5:15 PM |
makarius | rISABELLEca69be5f60fe: clarified messages: avoid duplicate Timing; | | Jul 11 2020, 5:08 PM |
makarius | rISABELLE940195fbb282: clarified messages; | | Jul 11 2020, 4:58 PM |
makarius | rISABELLE5c9984820caa: clarified signature; | | Jul 11 2020, 4:41 PM |
makarius | rISABELLE17a41deb5950: tuned; | | Jul 11 2020, 4:37 PM |
makarius | rISABELLE5469bacf5573: avoid duplicate Timing messages (see also 5c4800f6b25a); | | Jul 11 2020, 4:32 PM |
makarius | rISABELLE6c6609fd898c: more accurate message; | | Jul 11 2020, 4:25 PM |
makarius | rISABELLE2550bac18b49: tuned; | | Jul 11 2020, 3:52 PM |
makarius | rISABELLE6a24ecc4ff1b: clarified signature; | | Jul 11 2020, 3:51 PM |
makarius | rISABELLEc81e58a81b8c: clarified inlined protocol messages; | | Jul 11 2020, 3:23 PM |
makarius | rISABELLE0b1c830ebf3a: removed unused property; | | Jul 11 2020, 2:44 PM |
florian.haftmann | rAFP70ae335403b7: signed_take_bit | | Jul 11 2020, 8:21 AM |
florian.haftmann | rISABELLEa851ce626b78: signed_take_bit | | Jul 11 2020, 8:21 AM |
florian.haftmann | rISABELLEfebdd4eead56: more on single-bit operations | | Jul 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 |
makarius | rISABELLE7a53fc156c2b: proper session Timing for build_history log file (see 5c4800f6b25a); | | Jul 10 2020, 10:46 PM |
makarius | rISABELLE5c4800f6b25a: more robust protocol for "Timing ..." messages, notably for pide_session=true; | | Jul 10 2020, 10:46 PM |
makarius | rISABELLE7a53fc156c2b: proper session Timing for build_history log file (see 5c4800f6b25a); | | Jul 10 2020, 10:38 PM |
makarius | rISABELLE13890356df78: clarified signature; | | Jul 10 2020, 9:58 PM |
makarius | rISABELLE751f371d6883: more robust, notably for isabelle_cronjob; | | Jul 10 2020, 9:30 PM |
makarius | rISABELLE11c46b8e91c0: more robust build_session protocol: allow prover process to terminate/crash… | | Jul 10 2020, 9:23 PM |
desharna | rAFPd04de3d51efb: Fix failing proofs after update to Metis 2.4 | | Jul 9 2020, 11:41 AM |
desharna | rISABELLE913162a47d9f: Update Metis to 2.4 | | Jul 9 2020, 11:39 AM |
makarius | rISABELLEa7e6ac2dfa58: updated to polyml-5.8.1-20200708: recent repository version for testing; | | Jul 8 2020, 4:35 PM |
makarius | rISABELLE5c4800f6b25a: more robust protocol for "Timing ..." messages, notably for pide_session=true; | | Jul 8 2020, 2:43 PM |
dcjm | rPOLYML196ac3bc7d11: Move the test for the result of PolyCompareArbitrary up to the top-level of… | | Jul 7 2020, 9:23 AM |
dcjm | rPOLYMLf186be011f67: Add PointerEq as a binary operation and reserve WordComparison for the tagged… | | Jul 6 2020, 6:23 PM |
blanchette | rISABELLE3e08311ada8e: removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible… | | Jul 6 2020, 4:52 PM |
dcjm | rPOLYMLfb10196d998b: Convert single bindings from mutual recursion into simple bindings. | | Jul 6 2020, 3:26 PM |
dcjm | rPOLYMLfb10196d998b: Convert single bindings from mutual recursion into simple bindings. | | Jul 6 2020, 3:26 PM |
dcjm | rPOLYML19d82db2c17d: Separate out the strongly-connected sets code from CODETREE_FUNCTIONS so it can… | | Jul 6 2020, 3:26 PM |
dcjm | rPOLYML744d14ffd49b: Fix bug found by Makarius in generated code. It seems to have been introduced… | | Jul 6 2020, 3:26 PM |
dcjm | rPOLYMLfb10196d998b: Convert single bindings from mutual recursion into simple bindings. | | Jul 6 2020, 2:40 PM |
dcjm | rPOLYMLa020d4b5f62b: The "setter" for a container refers to the container itself so any bindings… | | Jul 6 2020, 2:34 PM |
florian.haftmann | rAFP1cdcce397e9d: separation of traditional bit operations | | Jul 6 2020, 12:47 PM |
florian.haftmann | rISABELLE379d0c207c29: separation of traditional bit operations | | Jul 6 2020, 12:47 PM |
dcjm | rPOLYMLade5d57318f0: Fix function name: they're mutual bindings not mutable. | | Jul 6 2020, 9:40 AM |
dcjm | rPOLYMLd761f194071f: When analysing the usage pattern of a recursive function we need to consider… | | Jul 6 2020, 9:30 AM |
makarius | rISABELLE720b72513ae5: no pide_session on macos: avoid odd "hang" of remote_build_history; | | Jul 5 2020, 11:06 AM |
makarius | rISABELLEf43b08980f56: support generated preferences, i.e. non-strict system options; | | Jul 5 2020, 11:00 AM |
florian.haftmann | rAFPa03e9b5d8dc9: factored out auxiliary theory | | Jul 4 2020, 10:45 PM |
florian.haftmann | rISABELLE4a013c92a091: factored out auxiliary theory | | Jul 4 2020, 10:45 PM |
florian.haftmann | rISABELLEc7ac6d4f3914: prefer explicit proof | | Jul 4 2020, 10:45 PM |
Andreas Lochbihler | rAFPb5b8255ae4c4: more operations for maps | | Jul 4 2020, 4:25 PM |
makarius | rISABELLEcb7ddc321f52: tuned whitespace; | | Jul 3 2020, 5:11 PM |
makarius | rISABELLEbbec0acf2592: use less memory on old hardware; | | Jul 3 2020, 5:11 PM |
makarius | rISABELLE088e3aa85250: clarified signature; | | Jul 3 2020, 5:00 PM |
makarius | rISABELLEc8c3f4f0f68b: clarified log message (more uniform); | | Jul 3 2020, 4:48 PM |
florian.haftmann | rAFPf90f9d593a88: misc lemma tuning | | Jul 3 2020, 10:01 AM |
dcjm | rPOLYML7edf731ebd7f: Fix use of "print" rather than "stream" for debugging. | | Jul 3 2020, 9:36 AM |
florian.haftmann | rISABELLE8bff286878bf: misc lemma tuning | | Jul 3 2020, 8:18 AM |
florian.haftmann | rISABELLE66beb9d92e43: explicit proofs for bit projections | | Jul 3 2020, 8:18 AM |
florian.haftmann | rAFPe0714a129570: updated documentation | | Jul 2 2020, 4:27 PM |
florian.haftmann | rISABELLEbad75618fb82: extraction of equations x = t from premises beneath meta-all | | Jul 2 2020, 2:10 PM |
florian.haftmann | rAFP81a8bf702c09: activated simproc defined_all | | Jul 2 2020, 2:10 PM |
florian.haftmann | rISABELLEace45a11a45e: a small aggiornamento for Z2 | | Jul 2 2020, 10:49 AM |
florian.haftmann | rISABELLEec17263ec38d: removed superfluous dependency | | Jul 2 2020, 10:49 AM |
florian.haftmann | rAFPb8a6808299e5: obsolete duplicates | | Jul 2 2020, 10:41 AM |
makarius | rISABELLE694009ed4ee1: clarified options --- potentially more robust; | | Jul 1 2020, 10:11 PM |
makarius | rISABELLEcea6087e8a70: tuned message; | | Jul 1 2020, 9:14 PM |
florian.haftmann | rISABELLEa1cf296a7786: moved to Word_Lib | | Jul 1 2020, 7:32 PM |
florian.haftmann | rAFP3ceb3fe8ab08: factored out ancient numeral representation | | Jul 1 2020, 7:32 PM |
florian.haftmann | rAFP04f54c116f30: tuned whitespace | | Jul 1 2020, 7:32 PM |
florian.haftmann | rAFP82e10d1ca9e1: moved to Word_Lib | | Jul 1 2020, 7:32 PM |
florian.haftmann | rISABELLE76193dd4aec8: factored out ancient numeral representation | | Jul 1 2020, 7:32 PM |
florian.haftmann | rISABELLE10a8d943a8d8: more explicit proofs | | Jul 1 2020, 7:32 PM |
kleing | rAFPec1d5c638a9d: merge from afp-2020 | | Jul 1 2020, 4:01 AM |
kleing | rAFPe4d6b7cae35c: Update history commit links to Heptapod | | Jul 1 2020, 3:31 AM |
kleing | rAFP4d18e0481131: merge from afp-2020 | | Jul 1 2020, 3:10 AM |
kleing | rAFPb29dde548f6b: Error message update | | Jul 1 2020, 3:02 AM |
kleing | rAFPc6e3efe2d729: One more instance of Bitbucket in README | | Jul 1 2020, 3:01 AM |
kleing | rAFPd3f602e38421: remove Bitbucket from website | | Jul 1 2020, 2:59 AM |
kleing | rAFP331165f0b57c: Update editor instructions for Heptapod + clarifications | | Jul 1 2020, 2:43 AM |
kleing | rAFP0519b84e33aa: Convert maintenance instructions to Heptapod | | Jul 1 2020, 2:37 AM |
kleing | rAFPd78aafccfd60: Update README to Heptapod | | Jul 1 2020, 2:33 AM |
kleing | rAFP9dfda1e96dc6: Point publish script to heptapod | | Jul 1 2020, 2:33 AM |
Julian Brunner <julianbrunner@gmail.com> | rAFPca5b629f4e0a: merged | | Jun 29 2020, 2:42 PM |
kleing | rAFP87644ed179f4: Further Bitbucket -> Heptapod docs update | | Jun 29 2020, 2:38 PM |
Julian Brunner <julianbrunner@gmail.com> | rAFPf95fe1ab8980: refactoring | | Jun 29 2020, 10:33 AM |
Lars Hupel <lars.hupel@mytum.de> | rAFP2f442131b76e: exclude another session on Mac | | Jun 29 2020, 9:24 AM |
kleing | rAFP3b5ff4b8d37d: Closing branch "devel" | | Jun 29 2020, 6:07 AM |
kleing | rAFPa35807f8a56e: merge | | Jun 29 2020, 6:04 AM |
kleing | rAFPc0032d11a990: Bitbucket -> Heptapod | | Jun 29 2020, 4:45 AM |
kleing | rAFP238b15a87fd2: Update README for Heptapod | | Jun 29 2020, 2:40 AM |
GitHub <noreply@github.com> | rPOLYMLef44a8b94c08: Merge pull request #135 from pclayton/fix-largeword-fromint | | Jun 28 2020, 3:35 PM |
GitHub <noreply@github.com> | rPOLYML13efa88e9a1f: Merge pull request #122 from jrtc27/libffi-i386 | | Jun 28 2020, 2:57 PM |
makarius | rISABELLE0be06f99b210: clarified signature; | | Jun 27 2020, 11:25 AM |
makarius | rISABELLE6441b4591eb8: more CONTRIBUTORS; | | Jun 26 2020, 5:34 PM |
makarius | rWEBSITE372d301ab6b6: updated URL (auto-forwarded); | | Jun 26 2020, 5:02 PM |
makarius | T12: Hosting of Isabelle/AFP after Jun-2020 | | Jun 26 2020, 4:39 PM |