Page MenuHomeIsabelle/Phabricator
Feed All Transactions
AuthorObjectTransactionDate
makariusrISABELLEff0e0bb81597: support for idea-icons (using ideaIC-129.354/platform/icons/src from IntelliJ…May 10 2021, 5:14 PM
makariusrISABELLE0476728f2887: mergedMay 10 2021, 4:26 PM
makariusrISABELLE26a1d66b9077: tuned proofs --- avoid z3, which is absent on arm64-linux;May 10 2021, 4:14 PM
dcjmrPOLYML9ed71255ccc0: Don't check for libgcc and libgcc_s. They will be included anyway if needed.May 10 2021, 3:31 PM
makariusrISABELLE6e85281177df: proper condition: z3 could be absent, e.g. on arm64-linux;May 10 2021, 2:28 PM
dcjmrPOLYML86dceaac467b: Rebuild configure after last change.May 10 2021, 1:12 PM
dcjmrPOLYML720f2cf1ad03: Rework the locking for profiling.May 10 2021, 1:08 PM
makariusrISABELLEd9823224fcfe: 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
Walter Guttmann <walter.guttmann@canterbury.ac.nz> committed rAFPc1ea0881dab4: Relational_Minimum_Spanning_Trees: refactoring Boruvka.thy. 
May 10 2021, 8:15 AM
paulson <lp15@cam.ac.uk>rAFP54d98b691624: more tiny tweaks
paulson <lp15@cam.ac.uk> committed rAFP54d98b691624: more tiny tweaks. 
May 9 2021, 5:30 PM
florian.haftmannrAFPf8ded3c69c5d: more elementary swapMay 9 2021, 7:48 AM
florian.haftmannrISABELLE1bd3463e30b8: more elementary swapMay 9 2021, 7:48 AM
dcjmrPOLYMLa2e8a53cf44f: Handle re-exporting code with ADRP/LDR sequence.May 8 2021, 6:44 PM
makariusrISABELLEd5c3eee7da74: separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597);May 8 2021, 1:06 PM
makariusrISABELLE4fbbf421c376: tuned message;May 8 2021, 12:31 AM
makariusrISABELLE9ce115baaa4f: clarified signature;May 7 2021, 11:56 PM
makariusrISABELLE029de1598940: tuned signature;May 7 2021, 9:03 PM
paulsonrAFP3e3ac2ce9873: merged
paulson committed rAFP3e3ac2ce9873: merged. 
May 7 2021, 5:51 PM
paulson <lp15@cam.ac.uk>rAFP9793065dd1c9: slight tidying of 1.19
paulson <lp15@cam.ac.uk> committed rAFP9793065dd1c9: slight tidying of 1.19. 
May 7 2021, 5:51 PM
makariusrISABELLEa037f01aedab: tuned comments;May 7 2021, 4:49 PM
makariusrISABELLE078ad17eb934: misc updates and clarification;May 7 2021, 4:45 PM
makariusrISABELLEdea7f6a2485e: clarified file name;May 7 2021, 4:44 PM
makariusrISABELLE0da9e824255f: mergedMay 7 2021, 1:37 PM
makariusrISABELLE9b4579e5bced: updated to polyml-5.8.2 (official release);May 7 2021, 1:34 PM
makariusrISABELLEac6f8fff036b: clarified default_platform_families (again);May 7 2021, 1:17 PM
makariusrISABELLEa2d3b4a90bca: proper option for linux_arm;May 7 2021, 1:16 PM
dcjmrPOLYML48ca209fd6a1: Rebuilt after merge.May 7 2021, 12:54 PM
dcjmrPOLYML3af934b6e907: Merge branch 'master' into ARMMerge2May 7 2021, 12:52 PM
makariusrISABELLEf4778e08dcd7: proper "$?";May 7 2021, 12:43 PM
dcjmrPOLYMLe6a463e1614f: Merge branch 'Endian5.8.2' into fixes-5.8.2. Fixes #150May 7 2021, 12:26 PM
makariusrISABELLEe1432539df35: proper jvm_platform, notably for org.sqlite.lib.path;May 6 2021, 11:28 PM
makariusrISABELLEa6a9162f3ec1: tuned message;May 6 2021, 11:20 PM
makariusrISABELLEf3a356c64193: support for platform family "linux_arm";May 6 2021, 11:09 PM
makariusrISABELLE6945ac084763: clarified purge;May 6 2021, 10:13 PM
makariusrAFP718639187389: no hardwired document;May 6 2021, 10:05 PM
makariusrISABELLE3531d20cf2fd: removed junk;May 6 2021, 8:54 PM
makariusrISABELLEc88faa1e09e1: support local build_heaps;May 6 2021, 8:43 PM
dcjmrPOLYMLfb4c91ba3ac1: Rebuilt pre-built compiler with endian fix.May 6 2021, 9:43 AM
dcjmrPOLYML87de1f409494: Only call PolyIsBigEndian when the code segment is being created. It was…May 6 2021, 9:37 AM
makariusrISABELLE7e465e166bb2: mergedMay 5 2021, 9:14 PM
makariusrISABELLE7c70f10e0b3b: tuned --- rename = dist_name is sufficient;May 5 2021, 8:41 PM
makariusrISABELLEf17caa5002df: proper dist_name;May 5 2021, 8:37 PM
florian.haftmannrAFPf9dd3b4a6fd5: tuned theory structureMay 5 2021, 6:09 PM
florian.haftmannrISABELLE4dc3baf45d6a: more appropriate locationMay 5 2021, 6:09 PM
florian.haftmannrISABELLE5020054b3a16: tuned theory structureMay 5 2021, 6:09 PM
paulsonrAFPc272e0d255f2: merged
paulson committed rAFPc272e0d255f2: merged. 
May 5 2021, 5:30 PM
paulson <lp15@cam.ac.uk>rAFP5b179b8ac1fa: more proof tidying
paulson <lp15@cam.ac.uk> committed rAFP5b179b8ac1fa: more proof tidying. 
May 5 2021, 5:30 PM
makariusrISABELLEf2e836e013cb: clarified option -P: allow empty argument;May 5 2021, 2:17 PM
makariusrISABELLEa771807df752: support for existing release archive;May 5 2021, 2:07 PM
makariusrISABELLEac8feb094bd4: tuned signature;May 5 2021, 1:30 PM
makariusrISABELLE27659455c592: clarified signature;May 5 2021, 1:27 PM
makariusrISABELLE0732f66ce514: more website content;May 4 2021, 8:40 PM
makariusrISABELLEf8f065e20837: misc tuning and clarification: more explicit types Release_Context…May 4 2021, 8:02 PM
florian.haftmannrAFP6cf5bfc61f4b: collected lemmas on permutationsMay 4 2021, 7:57 PM
florian.haftmannrISABELLEb4b70d13c995: collected lemmas on permutationsMay 4 2021, 7:57 PM
paulsonrAFP30f9c323e6d0: merged
paulson committed rAFP30f9c323e6d0: merged. 
May 4 2021, 6:01 PM
paulson <lp15@cam.ac.uk>rAFPedae802b7d54: simpler proofs of stronger lemmas
paulson <lp15@cam.ac.uk> committed rAFPedae802b7d54: simpler proofs of stronger lemmas. 
May 4 2021, 6:00 PM
dcjmrPOLYML42ada6abe712: Remove 5.8.1 compatibility files.May 4 2021, 12:58 PM
makariusrISABELLEf033d4f661e9: tuned signature;May 4 2021, 12:54 PM
Asta Halkjær From <andro.from@gmail.com>rAFP6a7d4e617b10: Tweaks
Asta Halkjær From <andro.from@gmail.com> committed rAFP6a7d4e617b10: Tweaks. 
May 4 2021, 12:40 PM
Rene Thiemann <rene.thiemann@uibk.ac.at>rAFPd119f1e8ad9a: restructure proof
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd119f1e8ad9a: restructure proof. 
May 4 2021, 12:16 PM
Rene Thiemann <rene.thiemann@uibk.ac.at>rAFPd217041e01ee: tuned proofs
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd217041e01ee: tuned proofs. 
May 4 2021, 10:27 AM
kleingrAFPe5d26217ccd3: update affiliationMay 4 2021, 3:54 AM
paulson <lp15@cam.ac.uk>rISABELLE58aed6f71f90: A nice cardinality lemma
paulson <lp15@cam.ac.uk> committed rISABELLE58aed6f71f90: A nice cardinality lemma. 
May 3 2021, 10:49 PM
Rene Thiemann <rene.thiemann@uibk.ac.at>rAFP9ff0da80391b: renamings
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP9ff0da80391b: renamings. 
May 3 2021, 8:37 PM
nipkowrAFP64cb55b26fa7: New entry: Regressioon_Test_SelectionMay 3 2021, 7:26 PM
nipkowrISABELLE0c8d6bec6491: tuned
nipkow committed rISABELLE0c8d6bec6491: tuned. 
May 3 2021, 7:06 PM
paulson <lp15@cam.ac.uk>rAFP15998112d738: just a few more tweaks
paulson <lp15@cam.ac.uk> committed 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 lemmaMay 3 2021, 3:32 PM
paulsonrAFPf4ec023a9857: merged
paulson committed rAFPf4ec023a9857: merged. 
May 2 2021, 11:14 PM
paulson <lp15@cam.ac.uk>rAFP67e4f5da18f4: some revisions to Lemma 3.7
paulson <lp15@cam.ac.uk> committed rAFP67e4f5da18f4: some revisions to Lemma 3.7. 
May 2 2021, 11:14 PM
makariusrISABELLE4b413b78cd94: more robust indentation: proper line context after insert;May 2 2021, 9:46 PM
makariusrISABELLE20d0abffee99: more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().May 2 2021, 8:51 PM
makariusrISABELLEb0ea03e837b1: support nested cases;May 2 2021, 5:38 PM
makariusrISABELLEe768759ce6c5: tuned;May 2 2021, 3:56 PM
makariusrISABELLE14757eb3b249: tuned;May 2 2021, 3:22 PM
makariusrISABELLEc1d8cd6d1a49: early definition of ML antiquotations;May 2 2021, 2:07 PM
dcjmrPOLYMLf84689bde7d2: Pre-built compilers for X86/64 Windows and X86/64-32 Windows.May 2 2021, 1:53 PM
dcjmrPOLYML7a7bc0fec7f7: 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
n.muendler <n.muendler@tum.de> committed rAFP8d3f34246608: Formatting, remove wrongly added file. 
May 2 2021, 1:45 PM
dcjmrPOLYMLad51084b76de: Built pre-built compilers for X86/32 and 32-bit interpreted.May 2 2021, 1:33 PM
dcjmrPOLYML049bf0dc36a7: Rebuilt compilers for SYSV X86/64, X86/64-32 and 64-bit interpreted.May 2 2021, 1:09 PM
dcjmrPOLYML1fd2fd8e59d6: Rebuilt confure for new release.May 2 2021, 12:54 PM
paulsonrAFP943298de494d: merged
paulson committed rAFP943298de494d: merged. 
May 2 2021, 11:56 AM
paulson <lp15@cam.ac.uk>rAFPe817fd6032e3: small refinements to partition proofs
paulson <lp15@cam.ac.uk> committed 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 entryMay 2 2021, 3:04 AM
makariusrISABELLEf28df88c0d00: tuned;May 1 2021, 11:54 AM
Rene Thiemann <rene.thiemann@uibk.ac.at>rAFP1edcb594d89c: cleaning proofs, use more real_asymp
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP1edcb594d89c: cleaning proofs, use more real_asymp. 
Apr 30 2021, 1:08 PM
makariusrISABELLEcc36841eeff6: 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 lemmasApr 29 2021, 6:14 PM
makariusrISABELLE6ba5f9d18c56: clarified signature: more operations;Apr 29 2021, 3:49 PM
dcjmrPOLYML46cc895e6bf9: Update version numbers ready for release of 5.8.2Apr 29 2021, 2:33 PM
dcjmrPOLYMLe87c60deeb72: Check arity of constructors in where type before trying to apply realisation.Apr 29 2021, 1:59 PM
makariusrISABELLE58b17dca57ef: clarified signature;Apr 28 2021, 11:20 PM
paulsonrAFP94431ee73ba6: merged
paulson committed rAFP94431ee73ba6: merged. 
Apr 28 2021, 7:19 PM
paulson <lp15@cam.ac.uk>rAFP9ae2386150de: trying to streamline a few proofs
paulson <lp15@cam.ac.uk> committed 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
Fabian Huch <huch@in.tum.de> committed rAFPece820d5ecd3: feat(sitegen-devel): switched to python3. 
Apr 28 2021, 5:34 PM
makariusrISABELLE6081885b9d06: tuned signature;Apr 28 2021, 2:03 PM
dcjmrPOLYML16458adbf40e: 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
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP5ad4e75b14a4: renamings to ensure consistency with paper description. 
Apr 28 2021, 1:09 PM