| Author | Object | Transaction | Date |
|---|
| makarius | rISABELLEfc13738e1933: clarified command-line, following other build_XYZ tools; | | Apr 28 2021, 1:03 PM |
| makarius | rISABELLE460e7535df46: more recent OCaml and GHC stack: better support for Apple Silicon; | | Apr 28 2021, 12:24 PM |
| Andreas Lochbihler <mail@andreas-lochbihler.de> | rAFP073e8a114c2e: metadata for Metalogic_ProofChecker | | Apr 28 2021, 10:21 AM |
| Andreas Lochbihler <mail@andreas-lochbihler.de> | rAFP8e9ea5fc7383: new entry Metalogic_ProofChecker | | Apr 28 2021, 10:17 AM |
| Andreas Lochbihler <mail@andreas-lochbihler.de> | rAFPa806650b5376: metadata for GaleStewart_Games | | Apr 28 2021, 10:11 AM |
| Andreas Lochbihler <mail@andreas-lochbihler.de> | rAFPb388d0d42d35: new entry GaleStewart_Games | | Apr 28 2021, 10:05 AM |
| kleing | rAFPa3e47d69f0c9: regen website | | Apr 28 2021, 9:46 AM |
| Simon Wimmer <wimmers@in.tum.de> | rAFP1a8521c8ed48: Merged | | Apr 27 2021, 11:55 PM |
| Simon Wimmer <wimmers@in.tum.de> | rAFP1a0b2d73ec78: Monad_Memo_DP: curry opt_bst and slight tuning | | Apr 27 2021, 11:55 PM |
| dcjm | rPOLYMLd233f6d4b8eb: Fix indexing of vectors and arrays for PackReal32 on 64-bits. | | Apr 27 2021, 9:55 AM |
| makarius | rISABELLE51f7bda1bfa2: merged | | Apr 25 2021, 10:33 PM |
| makarius | rISABELLE51b291ae3e2d: avoid "exec" to change the winpid; | | Apr 25 2021, 10:33 PM |
| makarius | rISABELLE342362c9496c: clarified check of root process on Windows (NB: the winpid is less stable than… | | Apr 25 2021, 9:12 PM |
| paulson <lp15@cam.ac.uk> | rAFPc05cd976ec65: fixed the ROOT file ofr BenOr_Kozen_Reif | | Apr 25 2021, 5:27 PM |
| paulson <lp15@cam.ac.uk> | rAFPec17a4428a60: webpage for BenOr_Kozen_Reif | | Apr 25 2021, 5:15 PM |
| paulson <lp15@cam.ac.uk> | rAFP149d79fb9a89: new entry BenOr_Kozen_Reif | | Apr 25 2021, 5:05 PM |
| dcjm | rPOLYML57acf78cc22e: Fix type-dependent functions, e.g. PolyML.print, if they were in a structure… | | Apr 23 2021, 5:44 PM |
| florian.haftmann | rAFP28fe4ca859cd: collecting more lemmas concerning multisets | | Apr 23 2021, 11:50 AM |
| florian.haftmann | rISABELLE5c4a09c4bc9c: collecting more lemmas concerning multisets | | Apr 23 2021, 11:50 AM |
| makarius | rISABELLE37243ad3ecb6: fast approximation of test for process group (NB: initial process might already… | | Apr 22 2021, 11:40 PM |
| makarius | rISABELLE19c558ea903c: clarified signature; | | Apr 22 2021, 11:03 PM |
| makarius | rISABELLE328392479308: rebuild executable for x86_64-darwin; | | Apr 22 2021, 10:55 PM |
| makarius | rISABELLE981df2e1f646: clarified command-line; | | Apr 22 2021, 10:07 PM |
| makarius | rISABELLE461da479f95c: update Linux base-line; | | Apr 22 2021, 10:04 PM |
| makarius | rISABELLE07a8ea094eb3: tuned comments; | | Apr 22 2021, 11:12 AM |
| makarius | rISABELLEe9e60be9928e: tuned signature; | | Apr 22 2021, 10:55 AM |
| makarius | rISABELLEaece5cc9efb7: simplified typesetting of \<guillemotleft>...\<guillemotright>; | | Apr 22 2021, 10:11 AM |
| lukasstevens | SSH Key 8 | | Apr 21 2021, 10:43 AM |
| lukasstevens | SSH Key 8 | lukasstevens updated the public key material for this SSH key. | Apr 21 2021, 10:43 AM |
| lukasstevens | SSH Key 8 | | Apr 21 2021, 10:43 AM |
| makarius | rISABELLEe60333aa18ca: proper use of antiquotations; | | Apr 20 2021, 10:53 PM |
| makarius | rAFPf8e89e956d62: more realistic timeout; | | Apr 20 2021, 12:55 PM |
| makarius | rAFP1ac0a5987165: tuned whitespace; | | Apr 20 2021, 12:16 PM |
| Asta Halkjær From <andro.from@gmail.com> | rAFP1df7aedab89d: Tweaks | | Apr 20 2021, 10:17 AM |
| makarius | rISABELLEc642c3cbbf0e: more documentation on "Conversions"; | | Apr 19 2021, 9:57 PM |
| makarius | rAFPa32a85449094: adapted to Isabelle/a2c589d5e1e4; | | Apr 19 2021, 7:26 PM |
| makarius | rISABELLEa2c589d5e1e4: clarified signature: more detailed token positions for antiquotations; | | Apr 19 2021, 7:26 PM |
| makarius | rAFPa32a85449094: adapted to Isabelle/a2c589d5e1e4; | | Apr 19 2021, 7:24 PM |
| paulson <lp15@cam.ac.uk> | rAFP74da145e496a: Merge | | Apr 19 2021, 6:40 PM |
| paulson <lp15@cam.ac.uk> | rAFP4dc8cb80716c: tweak | | Apr 19 2021, 6:39 PM |
| nipkow | rAFP88c78e611557: simplified proof | | Apr 19 2021, 4:59 PM |
| nipkow | rISABELLEc1f8aaa13ee3: tuned | | Apr 19 2021, 3:55 PM |
| paulson <lp15@cam.ac.uk> | rAFP141f2e614ae3: Slight tidying to shorten too-long lines | | Apr 19 2021, 11:48 AM |
| kleing | rAFP556e4a005c15: sshiftr/bl lemmas by Florian Märkl | | Apr 19 2021, 12:26 AM |
| paulson <lp15@cam.ac.uk> | rAFP1e065f54de8c: proof simplification | | Apr 18 2021, 8:03 PM |
| paulson <lp15@cam.ac.uk> | rAFPaf69398094b7: added a necessary acknowledgment (ERC) | | Apr 18 2021, 3:35 PM |
| dcjm | rPOLYML45c3b121901b: Convert int directly to Real32.real rather than via Real.real. Implement… | | Apr 18 2021, 12:29 PM |
| dcjm | rPOLYML7b73eeeddef2: Implement conversion from int to Real32.real directly for X86. This is needed… | | Apr 18 2021, 12:29 PM |
| dcjm | rPOLYML45c3b121901b: Convert int directly to Real32.real rather than via Real.real. Implement… | | Apr 18 2021, 12:29 PM |
| dcjm | rPOLYMLf0894d4c28af: Implement conversion from int to Real32.real directly for X86. This is needed… | | Apr 18 2021, 12:29 PM |
| paulson <lp15@cam.ac.uk> | rAFP712e90c69be4: cosmetic tweaks to proofs | | Apr 17 2021, 9:50 PM |
| makarius | rISABELLE1aa9ef7a3eaf: updated example; | | Apr 17 2021, 7:47 PM |
| makarius | rISABELLE479e9b17090e: clarified options (again); | | Apr 17 2021, 7:45 PM |
| makarius | rISABELLEa96de8bbe8a3: more options: update ISABELLE_IDENTIFIER; | | Apr 17 2021, 7:37 PM |
| dcjm | rPOLYML568d4ed99d86: Merge remote-tracking branch 'remotes/origin/master' into ARM64Testing | | Apr 17 2021, 9:52 AM |
| makarius | rISABELLEd1767bcb79ec: clarified conditional ML; | | Apr 16 2021, 11:35 PM |
| makarius | rISABELLE76d0b6597c91: support for conditional ML text; | | Apr 16 2021, 11:16 PM |
| makarius | rISABELLE386416437ce9: updated example; | | Apr 16 2021, 9:54 PM |
| makarius | rISABELLE1d4c9fa00821: clarified options; | | Apr 16 2021, 9:50 PM |
| dcjm | rPOLYMLd621a0b55b42: Reinstate tests on the command argument to Unix.execute to check it is… | | Apr 16 2021, 6:53 PM |
| dcjm | rPOLYML752120226579: Implement Unix.executeInEnv and hence Unix.execute largely in C rather | | Apr 16 2021, 5:12 PM |
| nipkow | rAFP7cc207b26f4f: New entry Progress_Tracking | | Apr 16 2021, 7:27 AM |
| florian.haftmann | rISABELLEed5226fdf89d: proper context variable handling when stripping leadings quantifiers from test… | | Apr 15 2021, 9:45 PM |
| paulson | rAFP401da3b5743d: merged | | Apr 15 2021, 6:43 PM |
| paulson <lp15@cam.ac.uk> | rAFP075ee4dc645d: minor stylistic changes | | Apr 15 2021, 6:42 PM |
| Asta Halkjær From <andro.from@gmail.com> | rAFP77def7de7e09: Add completeness of modal logics T, KB, K4, S4 and S5 | | Apr 15 2021, 5:54 PM |
| paulson <lp15@cam.ac.uk> | rAFP8f1f310afd72: Stylistic tweaks, which I hope are improvements :-) | | Apr 15 2021, 2:12 PM |
| makarius | rISABELLEdabe295c3f62: proper etc/ISABELLE_ID from archive (amending 4cba4e250c28); | | Apr 14 2021, 10:52 PM |
| makarius | rISABELLE4cba4e250c28: clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos; | | Apr 14 2021, 10:52 PM |
| makarius | rISABELLEdabe295c3f62: proper etc/ISABELLE_ID from archive (amending 4cba4e250c28); | | Apr 14 2021, 9:15 PM |
| makarius | rISABELLEcd84e58aed26: eliminated perl: prefer elementary GNU printenv; | | Apr 14 2021, 8:53 PM |
| dcjm | rPOLYML9ce77e67c5df: Use a writable address when setting data in the new constant area. | | Apr 14 2021, 8:24 PM |
| dcjm | rPOLYMLe48478b040d4: Only include ARM64 relocations if we're building for ARM64. The defines may not… | | Apr 14 2021, 7:38 PM |
| dcjm | rPOLYML64ebde2f2000: malloc and free are in stdlib.h on OpenBSD. | | Apr 14 2021, 7:36 PM |
| dcjm | rPOLYML5626a120b132: When loading code containing an FFI callback update the global heap base… | | Apr 14 2021, 6:53 PM |
| makarius | rISABELLEa96564139fa7: more robust bootstrap of components; | | Apr 14 2021, 2:36 PM |
| makarius | rISABELLE8ddf6728ad80: more self-contained support for macOS; | | Apr 14 2021, 2:28 PM |
| dcjm | rPOLYMLceb103ce85e0: Some fixes for Unix. | | Apr 14 2021, 2:06 PM |
| dcjm | rPOLYML0fe9c8778860: Reorganise OS memory allocators. | | Apr 14 2021, 1:51 PM |
| dcjm | rPOLYML3473d907422e: Merge branch 'SeparateCodeAndConsts' into ARM64Merge | | Apr 14 2021, 9:12 AM |
| dcjm | rPOLYMLe0a8e77b0e35: Merge branch 'AllocateInContiguous' into SeparateCodeAndConsts | | Apr 14 2021, 9:11 AM |
| dcjm | rPOLYMLf2ba7eb15fc6: Update a relative address constant if it has moved even if it goes to the same… | | Apr 14 2021, 9:10 AM |
| paulson <lp15@cam.ac.uk> | rAFP04ce41144de1: Revisions by Wenda to eliminate the locale comp_affine_scheme | | Apr 13 2021, 7:18 PM |
| makarius | rISABELLE629868f96c81: misc tuning and clarification; | | Apr 13 2021, 4:19 PM |
| paulson <lp15@cam.ac.uk> | rAFP7d686b4e8472: renamed a lemma | | Apr 13 2021, 1:26 PM |
| dcjm | rPOLYML6a0adb9218a0: Implement callbacks (FFI closures) in ARM64. There is still a problem with… | | Apr 13 2021, 1:12 PM |
| paulson <lp15@cam.ac.uk> | rAFPa3ee7515305a: Fixed an error in the statement of closed_subsets_empty. Also added syntax… | | Apr 13 2021, 12:59 PM |
| makarius | rISABELLE6c8fc3c038eb: tuned signature; | | Apr 13 2021, 11:44 AM |
| traytel | rAFPbf041f4c01bf: updated paper references | | Apr 13 2021, 9:24 AM |
| makarius | rISABELLEa021bb558feb: clarified message output: flush already happens in write_message_yxml (see… | | Apr 12 2021, 11:26 PM |
| makarius | rISABELLE22b5ecb53dd9: more uniform use of Byte_Message; | | Apr 12 2021, 11:26 PM |
| makarius | rISABELLEd201996f72a8: provide CharSequence operations as well; | | Apr 12 2021, 11:26 PM |
| makarius | rISABELLEc83152933579: clarified signature: Bytes extends CharSequence already (see d201996f72a8); | | Apr 12 2021, 11:26 PM |
| makarius | rISABELLEb50f8cc8c08e: support for base64 via Isabelle/Scala/ML; | | Apr 12 2021, 10:57 PM |
| makarius | rISABELLE23d2adc5489e: compile; | | Apr 12 2021, 10:45 PM |
| makarius | rISABELLE12b3f78dde61: clarified signature: avoid overlap of String vs. Bytes (both are CharSequence); | | Apr 12 2021, 10:41 PM |
| makarius | rISABELLEa30a60aef59f: clarified signature (again); | | Apr 12 2021, 10:36 PM |
| makarius | rISABELLE6ab97ac63809: merged | | Apr 12 2021, 10:26 PM |
| makarius | rISABELLEf86661e32bed: clarified signature; | | Apr 12 2021, 10:26 PM |
| makarius | rISABELLEe21aef453cd4: unused; | | Apr 12 2021, 10:18 PM |