Author | Object | Transaction | Date |
---|
makarius | rISABELLEff0e0bb81597: support for idea-icons (using ideaIC-129.354/platform/icons/src from IntelliJ… | | May 10 2021, 5:14 PM |
makarius | rISABELLE0476728f2887: merged | | May 10 2021, 4:26 PM |
makarius | rISABELLE26a1d66b9077: tuned proofs --- avoid z3, which is absent on arm64-linux; | | May 10 2021, 4:14 PM |
dcjm | rPOLYML9ed71255ccc0: Don't check for libgcc and libgcc_s. They will be included anyway if needed. | | May 10 2021, 3:31 PM |
makarius | rISABELLE6e85281177df: proper condition: z3 could be absent, e.g. on arm64-linux; | | May 10 2021, 2:28 PM |
dcjm | rPOLYML86dceaac467b: Rebuild configure after last change. | | May 10 2021, 1:12 PM |
dcjm | rPOLYML720f2cf1ad03: Rework the locking for profiling. | | May 10 2021, 1:08 PM |
makarius | rISABELLEd9823224fcfe: build auxiliary jEdit component in Isabelle/Scala; | | May 10 2021, 12:23 PM |
Walter Guttmann <walter.guttmann@canterbury.ac.nz> | rAFPc1ea0881dab4: Relational_Minimum_Spanning_Trees: refactoring Boruvka.thy | | May 10 2021, 8:15 AM |
paulson <lp15@cam.ac.uk> | rAFP54d98b691624: more tiny tweaks | | May 9 2021, 5:30 PM |
florian.haftmann | rAFPf8ded3c69c5d: more elementary swap | | May 9 2021, 7:48 AM |
florian.haftmann | rISABELLE1bd3463e30b8: more elementary swap | | May 9 2021, 7:48 AM |
dcjm | rPOLYMLa2e8a53cf44f: Handle re-exporting code with ADRP/LDR sequence. | | May 8 2021, 6:44 PM |
makarius | rISABELLEd5c3eee7da74: separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597); | | May 8 2021, 1:06 PM |
makarius | rISABELLE4fbbf421c376: tuned message; | | May 8 2021, 12:31 AM |
makarius | rISABELLE9ce115baaa4f: clarified signature; | | May 7 2021, 11:56 PM |
makarius | rISABELLE029de1598940: tuned signature; | | May 7 2021, 9:03 PM |
paulson | rAFP3e3ac2ce9873: merged | | May 7 2021, 5:51 PM |
paulson <lp15@cam.ac.uk> | rAFP9793065dd1c9: slight tidying of 1.19 | | May 7 2021, 5:51 PM |
makarius | rISABELLEa037f01aedab: tuned comments; | | May 7 2021, 4:49 PM |
makarius | rISABELLE078ad17eb934: misc updates and clarification; | | May 7 2021, 4:45 PM |
makarius | rISABELLEdea7f6a2485e: clarified file name; | | May 7 2021, 4:44 PM |
makarius | rISABELLE0da9e824255f: merged | | May 7 2021, 1:37 PM |
makarius | rISABELLE9b4579e5bced: updated to polyml-5.8.2 (official release); | | May 7 2021, 1:34 PM |
makarius | rISABELLEac6f8fff036b: clarified default_platform_families (again); | | May 7 2021, 1:17 PM |
makarius | rISABELLEa2d3b4a90bca: proper option for linux_arm; | | May 7 2021, 1:16 PM |
dcjm | rPOLYML48ca209fd6a1: Rebuilt after merge. | | May 7 2021, 12:54 PM |
dcjm | rPOLYML3af934b6e907: Merge branch 'master' into ARMMerge2 | | May 7 2021, 12:52 PM |
makarius | rISABELLEf4778e08dcd7: proper "$?"; | | May 7 2021, 12:43 PM |
dcjm | rPOLYMLe6a463e1614f: Merge branch 'Endian5.8.2' into fixes-5.8.2. Fixes #150 | | May 7 2021, 12:26 PM |
makarius | rISABELLEe1432539df35: proper jvm_platform, notably for org.sqlite.lib.path; | | May 6 2021, 11:28 PM |
makarius | rISABELLEa6a9162f3ec1: tuned message; | | May 6 2021, 11:20 PM |
makarius | rISABELLEf3a356c64193: support for platform family "linux_arm"; | | May 6 2021, 11:09 PM |
makarius | rISABELLE6945ac084763: clarified purge; | | May 6 2021, 10:13 PM |
makarius | rAFP718639187389: no hardwired document; | | May 6 2021, 10:05 PM |
makarius | rISABELLE3531d20cf2fd: removed junk; | | May 6 2021, 8:54 PM |
makarius | rISABELLEc88faa1e09e1: support local build_heaps; | | May 6 2021, 8:43 PM |
dcjm | rPOLYMLfb4c91ba3ac1: Rebuilt pre-built compiler with endian fix. | | May 6 2021, 9:43 AM |
dcjm | rPOLYML87de1f409494: Only call PolyIsBigEndian when the code segment is being created. It was… | | May 6 2021, 9:37 AM |
makarius | rISABELLE7e465e166bb2: merged | | May 5 2021, 9:14 PM |
makarius | rISABELLE7c70f10e0b3b: tuned --- rename = dist_name is sufficient; | | May 5 2021, 8:41 PM |
makarius | rISABELLEf17caa5002df: proper dist_name; | | May 5 2021, 8:37 PM |
florian.haftmann | rAFPf9dd3b4a6fd5: tuned theory structure | | May 5 2021, 6:09 PM |
florian.haftmann | rISABELLE4dc3baf45d6a: more appropriate location | | May 5 2021, 6:09 PM |
florian.haftmann | rISABELLE5020054b3a16: tuned theory structure | | May 5 2021, 6:09 PM |
paulson | rAFPc272e0d255f2: merged | | May 5 2021, 5:30 PM |
paulson <lp15@cam.ac.uk> | rAFP5b179b8ac1fa: more proof tidying | | May 5 2021, 5:30 PM |
makarius | rISABELLEf2e836e013cb: clarified option -P: allow empty argument; | | May 5 2021, 2:17 PM |
makarius | rISABELLEa771807df752: support for existing release archive; | | May 5 2021, 2:07 PM |
makarius | rISABELLEac8feb094bd4: tuned signature; | | May 5 2021, 1:30 PM |
makarius | rISABELLE27659455c592: clarified signature; | | May 5 2021, 1:27 PM |
makarius | rISABELLE0732f66ce514: more website content; | | May 4 2021, 8:40 PM |
makarius | rISABELLEf8f065e20837: misc tuning and clarification: more explicit types Release_Context… | | May 4 2021, 8:02 PM |
florian.haftmann | rAFP6cf5bfc61f4b: collected lemmas on permutations | | May 4 2021, 7:57 PM |
florian.haftmann | rISABELLEb4b70d13c995: collected lemmas on permutations | | May 4 2021, 7:57 PM |
paulson | rAFP30f9c323e6d0: merged | | May 4 2021, 6:01 PM |
paulson <lp15@cam.ac.uk> | rAFPedae802b7d54: simpler proofs of stronger lemmas | | May 4 2021, 6:00 PM |
dcjm | rPOLYML42ada6abe712: Remove 5.8.1 compatibility files. | | May 4 2021, 12:58 PM |
makarius | rISABELLEf033d4f661e9: tuned signature; | | May 4 2021, 12:54 PM |
Asta Halkjær From <andro.from@gmail.com> | rAFP6a7d4e617b10: Tweaks | | May 4 2021, 12:40 PM |
Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPd119f1e8ad9a: restructure proof | | May 4 2021, 12:16 PM |
Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPd217041e01ee: tuned proofs | | May 4 2021, 10:27 AM |
kleing | rAFPe5d26217ccd3: update affiliation | | May 4 2021, 3:54 AM |
paulson <lp15@cam.ac.uk> | rISABELLE58aed6f71f90: A nice cardinality lemma | | May 3 2021, 10:49 PM |
Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP9ff0da80391b: renamings | | May 3 2021, 8:37 PM |
nipkow | rAFP64cb55b26fa7: New entry: Regressioon_Test_Selection | | May 3 2021, 7:26 PM |
nipkow | rISABELLE0c8d6bec6491: tuned | | May 3 2021, 7:06 PM |
paulson <lp15@cam.ac.uk> | rAFP15998112d738: just a few more tweaks | | May 3 2021, 6:40 PM |
Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP49921165cef0: lemma poly_asymp_equiv + simplified existing proof based on this lemma | | May 3 2021, 3:32 PM |
paulson | rAFPf4ec023a9857: merged | | May 2 2021, 11:14 PM |
paulson <lp15@cam.ac.uk> | rAFP67e4f5da18f4: some revisions to Lemma 3.7 | | May 2 2021, 11:14 PM |
makarius | rISABELLE4b413b78cd94: more robust indentation: proper line context after insert; | | May 2 2021, 9:46 PM |
makarius | rISABELLE20d0abffee99: more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet(). | | May 2 2021, 8:51 PM |
makarius | rISABELLEb0ea03e837b1: support nested cases; | | May 2 2021, 5:38 PM |
makarius | rISABELLEe768759ce6c5: tuned; | | May 2 2021, 3:56 PM |
makarius | rISABELLE14757eb3b249: tuned; | | May 2 2021, 3:22 PM |
makarius | rISABELLEc1d8cd6d1a49: early definition of ML antiquotations; | | May 2 2021, 2:07 PM |
dcjm | rPOLYMLf84689bde7d2: Pre-built compilers for X86/64 Windows and X86/64-32 Windows. | | May 2 2021, 1:53 PM |
dcjm | rPOLYML7a7bc0fec7f7: Fix 32-bit pre-built compilers wrongly built. | | May 2 2021, 1:50 PM |
n.muendler <n.muendler@tum.de> | rAFP8d3f34246608: Formatting, remove wrongly added file | | May 2 2021, 1:45 PM |
dcjm | rPOLYMLad51084b76de: Built pre-built compilers for X86/32 and 32-bit interpreted. | | May 2 2021, 1:33 PM |
dcjm | rPOLYML049bf0dc36a7: Rebuilt compilers for SYSV X86/64, X86/64-32 and 64-bit interpreted. | | May 2 2021, 1:09 PM |
dcjm | rPOLYML1fd2fd8e59d6: Rebuilt confure for new release. | | May 2 2021, 12:54 PM |
paulson | rAFP943298de494d: merged | | May 2 2021, 11:56 AM |
paulson <lp15@cam.ac.uk> | rAFPe817fd6032e3: small refinements to partition proofs | | May 2 2021, 11:55 AM |
n.muendler <n.muendler@tum.de> | rAFP6b5910524293: Add imperative deletion operation and OCaml code export to BTree entry | | May 2 2021, 3:04 AM |
makarius | rISABELLEf28df88c0d00: tuned; | | May 1 2021, 11:54 AM |
Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP1edcb594d89c: cleaning proofs, use more real_asymp | | Apr 30 2021, 1:08 PM |
makarius | rISABELLEcc36841eeff6: clarified signature: more operations; | | Apr 29 2021, 10:39 PM |
paulson <lp15@cam.ac.uk> | rAFP72edb20655d6: tiny bits of tidying up / simplification of proofs, aided by new lemmas | | Apr 29 2021, 6:14 PM |
makarius | rISABELLE6ba5f9d18c56: clarified signature: more operations; | | Apr 29 2021, 3:49 PM |
dcjm | rPOLYML46cc895e6bf9: Update version numbers ready for release of 5.8.2 | | Apr 29 2021, 2:33 PM |
dcjm | rPOLYMLe87c60deeb72: Check arity of constructors in where type before trying to apply realisation. | | Apr 29 2021, 1:59 PM |
makarius | rISABELLE58b17dca57ef: clarified signature; | | Apr 28 2021, 11:20 PM |
paulson | rAFP94431ee73ba6: merged | | Apr 28 2021, 7:19 PM |
paulson <lp15@cam.ac.uk> | rAFP9ae2386150de: trying to streamline a few proofs | | Apr 28 2021, 7:18 PM |
Fabian Huch <huch@in.tum.de> | rAFPece820d5ecd3: feat(sitegen-devel): switched to python3 | | Apr 28 2021, 5:34 PM |
makarius | rISABELLE6081885b9d06: tuned signature; | | Apr 28 2021, 2:03 PM |
dcjm | rPOLYML16458adbf40e: PolyML.pretty and PolyML.context are eqtypes based on their current… | | Apr 28 2021, 1:57 PM |
Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP5ad4e75b14a4: renamings to ensure consistency with paper description | | Apr 28 2021, 1:09 PM |