| Author | Object | Transaction | Date |
|---|
| makarius | rAFP75faf142b4be: eliminated odd clone (see Isabelle/caa5a257d3ed); | | May 16 2021, 7:43 PM |
| makarius | rISABELLE7c7a59b76528: recover some Linux test, using old macbroy2 as i21of4 (Ubuntu 20.04); | | May 16 2021, 7:37 PM |
| makarius | rISABELLE08def1cc6b33: avoid perl; | | May 16 2021, 4:05 PM |
| makarius | rISABELLE7202e12cb324: tuned signature --- following hints by IntelliJ IDEA; | | May 16 2021, 1:34 PM |
| makarius | rISABELLEd83e7e444b43: ignore session build timeout, notably in AFP; | | May 16 2021, 1:14 PM |
| makarius | rISABELLE908351c8c0b1: check timeout_ignored as in ML, before applying timeout_scale; | | May 16 2021, 1:06 PM |
| makarius | rISABELLE8ffc607c345d: added Mirabelle | | May 15 2021, 11:09 PM |
| makarius | rISABELLE8c4ba5f61223: unused (see 8ffc607c345d); | | May 15 2021, 11:09 PM |
| makarius | rISABELLEc74e25de3c00: merged | | May 15 2021, 10:39 PM |
| makarius | rISABELLE3d0952893db8: proper build of required session images vs. build with Mirabelle presentation; | | May 15 2021, 10:36 PM |
| makarius | rISABELLE0e7a5c7a14c8: reactive "sledgehammer"; | | May 15 2021, 10:06 PM |
| makarius | rISABELLE03e134d5f867: reactive "sledgehammer_filter": statically correct, but untested (no… | | May 15 2021, 5:40 PM |
| makarius | rISABELLEb6d444194280: clarified command-line; | | May 15 2021, 5:38 PM |
| makarius | rISABELLE60519a7bfc53: clarified signature; | | May 15 2021, 1:25 PM |
| dcjm | rPOLYML8ee44e4270dc: Fix longWordToTagged for big-endian 32-in-64. | | May 15 2021, 1:07 PM |
| dcjm | rPOLYMLde553b7fde0a: Fix incorrect mask in 8ee44e4. | | May 15 2021, 1:07 PM |
| dcjm | rPOLYMLc73509f16f52: Fix byte offset to flags in big-endian mode. The value in 201979c8 was wrong. | | May 15 2021, 1:07 PM |
| dcjm | rPOLYML201979c83114: The byte offset to the flags byte depends on whether this is big- or little… | | May 15 2021, 1:07 PM |
| makarius | rISABELLE3ab18af9b2b5: clarified signature; | | May 15 2021, 12:33 PM |
| makarius | rISABELLE8444d4ff5646: clarified log content; | | May 15 2021, 12:25 PM |
| makarius | rISABELLE2f9877db82a1: reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool… | | May 14 2021, 9:32 PM |
| pruvisto | rAFPcddbe565783d: sitegen for Padic_Ints | | May 14 2021, 5:51 PM |
| pruvisto | rAFPf463e6d25245: new entry: Padic_Ints | | May 14 2021, 5:14 PM |
| paulson <lp15@cam.ac.uk> | rAFPe93051f65b1a: strict_sorted now an abbreviation | | May 14 2021, 4:48 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE60a788467639: strict_sorted now an abbreviation | | May 14 2021, 1:43 PM |
| dcjm | rPOLYMLb928d20ac26f: Fix incorrect function names. | | May 14 2021, 1:15 PM |
| dcjm | rPOLYML24a06d603b74: Remove the test of GC in a forked child. This seems to fail badly on some… | | May 14 2021, 9:40 AM |
| dcjm | rPOLYMLaac4d1e94ad0: Replace usleep with nanosleep. Posix defines usleep to work only for values of… | | May 14 2021, 9:16 AM |
| dcjm | rPOLYML0e446f3e042c: Use shadow area if necessary when setting ARM relocations. | | May 13 2021, 9:11 PM |
| paulson | rAFP41cc428000e3: merged | | May 13 2021, 6:32 PM |
| paulson <lp15@cam.ac.uk> | rAFPa757f7e7c954: deleted needless material | | May 13 2021, 6:31 PM |
| dcjm | rPOLYMLc73509f16f52: Fix byte offset to flags in big-endian mode. The value in 201979c8 was wrong. | | May 13 2021, 4:55 PM |
| makarius | rISABELLE9267a04aabe6: tuned; | | May 13 2021, 3:52 PM |
| makarius | rISABELLEcaa5a257d3ed: unused; | | May 13 2021, 3:38 PM |
| dcjm | rPOLYMLde553b7fde0a: Fix incorrect mask in 8ee44e4. | | May 13 2021, 3:04 PM |
| dcjm | rPOLYML1a29bb7f55dd: Change argument type so that it is compatible with big-endian 32-in-64. | | May 13 2021, 2:50 PM |
| dcjm | rPOLYML8ee44e4270dc: Fix longWordToTagged for big-endian 32-in-64. | | May 13 2021, 2:14 PM |
| dcjm | rPOLYML2dc15cf77976: Fix interpreter after RTS function change. | | May 13 2021, 12:49 PM |
| paulson <lp15@cam.ac.uk> | rAFP8ff1ebba38da: more small simplifications | | May 12 2021, 11:20 PM |
| florian.haftmann | rAFPa055a33fcb58: next step to phase out ancient numerals | | May 12 2021, 7:05 PM |
| florian.haftmann | rAFPa19043a5f828: explicit type class operations for type-specific implementations | | May 12 2021, 7:05 PM |
| florian.haftmann | rISABELLE78044b2f001c: explicit type class operations for type-specific implementations | | May 12 2021, 7:05 PM |
| florian.haftmann | rISABELLE3708884bfa8a: obsolete | | May 12 2021, 7:05 PM |
| makarius | rISABELLE8c4ba5f61223: unused (see 8ffc607c345d); | | May 12 2021, 5:17 PM |
| makarius | rISABELLE54fe8cc0e1c6: clarified signature: provide access to previous state; | | May 12 2021, 4:47 PM |
| dcjm | rPOLYML18716c3f4dab: Fixes to Unix files after RTS function change. | | May 12 2021, 3:30 PM |
| dcjm | rPOLYML4aa7a6f54fc0: Change argument types of RTS functions so that they are always POLYUNSIGNED… | | May 12 2021, 3:17 PM |
| makarius | rISABELLEb9aae426e51d: clarified signature (see Scala version); | | May 12 2021, 2:55 PM |
| makarius | rISABELLEc17253cad5c6: tuned signature; | | May 12 2021, 1:10 PM |
| dcjm | rPOLYMLed789f849841: Fix name change omitted when this was last committed. | | May 12 2021, 1:08 PM |
| dcjm | rPOLYML601c48c6ad68: Updated 32-bit bootstrap file with support for big-endian. | | May 12 2021, 12:49 PM |
| makarius | rISABELLEa63d76ba0a03: avoid duplicate loading of ML file; | | May 12 2021, 12:22 PM |
| desharna | rISABELLE50437744eb1c: added lemmas map_ran_Cons_sel and (length|map_fst)_map_ran | | May 12 2021, 9:31 AM |
| nipkow | rISABELLE71c45d60a90a: merged | | May 12 2021, 6:35 AM |
| nipkow | rISABELLE78929c029785: generalized type | | May 11 2021, 10:40 PM |
| makarius | rISABELLE73c50ce808ed: basic setup of Isabelle setup tool --- pure Java, no dependencies; | | May 11 2021, 9:57 PM |
| makarius | rISABELLE51429b78aadf: merged | | May 11 2021, 9:21 PM |
| makarius | rISABELLE6c56f2ebe157: guess package more directly; | | May 11 2021, 8:19 PM |
| paulson | rAFP26d8da1ea081: merged | | May 11 2021, 7:59 PM |
| paulson <lp15@cam.ac.uk> | rAFPb383e59aa162: fixed some latex; tried the alternative definition of Ramsey | | May 11 2021, 7:59 PM |
| paulson | rISABELLE0d79ac2eb106: merged | | May 11 2021, 7:56 PM |
| dcjm | rPOLYMLa182946ad8e3: Have to take account of endian-ness when clearing ADR/LDR instruction offsets. | | May 11 2021, 6:18 PM |
| makarius | rISABELLE70d3c7009a65: proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64; | | May 11 2021, 4:55 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEedb01b64dc16: Just one lemma | | May 11 2021, 4:50 PM |
| makarius | rISABELLE7404f2e1d092: clarified platforms; | | May 11 2021, 4:30 PM |
| dcjm | rPOLYMLf2c0c9e261cd: Convert instruction values to little-endian when converting to ADRP/LDR. | | May 11 2021, 3:59 PM |
| dcjm | rPOLYMLfae25684e69e: Register mask is in an instruction and needs to be converted on big-endian. | | May 11 2021, 2:47 PM |
| makarius | rISABELLEff716ecb0805: put more resources into jedit_build component; | | May 11 2021, 2:29 PM |
| makarius | rISABELLE02351b514b34: proper jEdit.props (amending ff716ecb0805); | | May 11 2021, 2:29 PM |
| makarius | rISABELLE4121fc47432b: merged | | May 11 2021, 2:04 PM |
| makarius | rISABELLE02351b514b34: proper jEdit.props (amending ff716ecb0805); | | May 11 2021, 2:03 PM |
| makarius | rISABELLE5e12dad8d09b: update to gmp-6.2.1, with support for arm64-darwin; | | May 11 2021, 1:45 PM |
| dcjm | rPOLYML201979c83114: The byte offset to the flags byte depends on whether this is big- or little… | | May 11 2021, 1:20 PM |
| makarius | rISABELLE442460fba2a4: clarified platforms; | | May 11 2021, 1:06 PM |
| makarius | rISABELLE4d0df84a5b88: clarified options: implicitly support both x86_64 and arm64; | | May 11 2021, 12:21 PM |
| dcjm | rPOLYMLf2dce0a9fbd2: Constants and offsets need to be big-endian on big-endian architecture. | | May 11 2021, 12:15 PM |
| makarius | rISABELLE9ab1d5fa84d0: tuned whitespace; | | May 11 2021, 11:17 AM |
| dcjm | rPOLYML3f9b811f7c37: Convert between little-endian instruction format and native word. | | May 11 2021, 9:52 AM |
| dcjm | rPOLYML919fbd7d0a28: Support for NetBSD elf file. Work-around for misnamed(?) relocation symbol in… | | May 11 2021, 9:22 AM |
| dcjm | rPOLYMLdd4456fbd346: Updated bootstrap file for 64-bits with support for big-endian. | | May 11 2021, 9:14 AM |
| makarius | rISABELLE8b3e672df28c: proper build for fresh target directory (amending d9823224fcfe); | | May 10 2021, 10:58 PM |
| makarius | rISABELLEd9823224fcfe: build auxiliary jEdit component in Isabelle/Scala; | | May 10 2021, 10:58 PM |
| makarius | rISABELLEf6b453449cc6: more brackets; | | May 10 2021, 10:58 PM |
| makarius | rISABELLEaf82097b4adc: more brackets (see f6b453449cc6); | | May 10 2021, 10:58 PM |
| makarius | rISABELLE8b3e672df28c: proper build for fresh target directory (amending d9823224fcfe); | | May 10 2021, 10:32 PM |
| makarius | rISABELLEff716ecb0805: put more resources into jedit_build component; | | May 10 2021, 10:18 PM |
| florian.haftmann | rAFP0ace227c4d10: centralized more lemmas | | May 10 2021, 9:46 PM |
| florian.haftmann | rISABELLE6e26d06b24b1: centralized more lemmas | | May 10 2021, 9:46 PM |
| florian.haftmann | rAFPaac14245270a: avoid Fun.swap | | May 10 2021, 9:45 PM |
| florian.haftmann | rISABELLE7734c442802f: avoid Fun.swap | | May 10 2021, 9:45 PM |
| florian.haftmann | rAFP3945ab3f00b8: guide is out of focus | | May 10 2021, 9:45 PM |
| florian.haftmann | rISABELLEfecfb96474ca: guide is out of focus | | May 10 2021, 9:45 PM |
| paulson <lp15@cam.ac.uk> | rAFP9340467e8c9a: Trying out Ramsey_eq for simpler proofs | | May 10 2021, 9:45 PM |
| makarius | rISABELLEaf82097b4adc: more brackets (see f6b453449cc6); | | May 10 2021, 8:09 PM |
| dcjm | rPOLYMLf5dd6093d760: Merge branch 'master' into ARM64Testing | | May 10 2021, 6:58 PM |
| makarius | rISABELLEf6b453449cc6: more brackets; | | May 10 2021, 6:31 PM |
| makarius | rISABELLE6e85281177df: proper condition: z3 could be absent, e.g. on arm64-linux; | | May 10 2021, 5:35 PM |
| makarius | rISABELLEdceb5dde442f: proper settings variable, amending 6e85281177df; | | May 10 2021, 5:35 PM |
| makarius | rISABELLEdceb5dde442f: proper settings variable, amending 6e85281177df; | | May 10 2021, 5:15 PM |
| makarius | rISABELLEd5c3eee7da74: separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597); | | May 10 2021, 5:14 PM |