Page MenuHomeIsabelle/Phabricator
Feed All Transactions
AuthorObjectTransactionDate
makariusrAFP75faf142b4be: eliminated odd clone (see Isabelle/caa5a257d3ed);Sun, May 16, 7:47 PM
makariusrISABELLEcaa5a257d3ed: unused;Sun, May 16, 7:47 PM
makariusrAFP75faf142b4be: eliminated odd clone (see Isabelle/caa5a257d3ed);Sun, May 16, 7:43 PM
makariusrISABELLE7c7a59b76528: recover some Linux test, using old macbroy2 as i21of4 (Ubuntu 20.04);Sun, May 16, 7:37 PM
makariusrISABELLE08def1cc6b33: avoid perl;Sun, May 16, 4:05 PM
makariusrISABELLE7202e12cb324: tuned signature --- following hints by IntelliJ IDEA;Sun, May 16, 1:34 PM
makariusrISABELLEd83e7e444b43: ignore session build timeout, notably in AFP;Sun, May 16, 1:14 PM
makariusrISABELLE908351c8c0b1: check timeout_ignored as in ML, before applying timeout_scale;Sun, May 16, 1:06 PM
makariusrISABELLE8ffc607c345d: added MirabelleSat, May 15, 11:09 PM
makariusrISABELLE8c4ba5f61223: unused (see 8ffc607c345d);Sat, May 15, 11:09 PM
makariusrISABELLEc74e25de3c00: mergedSat, May 15, 10:39 PM
makariusrISABELLE3d0952893db8: proper build of required session images vs. build with Mirabelle presentation;Sat, May 15, 10:36 PM
makariusrISABELLE0e7a5c7a14c8: reactive "sledgehammer";Sat, May 15, 10:06 PM
makariusrISABELLE03e134d5f867: reactive "sledgehammer_filter": statically correct, but untested (no…Sat, May 15, 5:40 PM
makariusrISABELLEb6d444194280: clarified command-line;Sat, May 15, 5:38 PM
makariusrISABELLE60519a7bfc53: clarified signature;Sat, May 15, 1:25 PM
dcjmrPOLYML8ee44e4270dc: Fix longWordToTagged for big-endian 32-in-64.Sat, May 15, 1:07 PM
dcjmrPOLYMLde553b7fde0a: Fix incorrect mask in 8ee44e4.Sat, May 15, 1:07 PM
dcjmrPOLYMLc73509f16f52: Fix byte offset to flags in big-endian mode. The value in 201979c8 was wrong.Sat, May 15, 1:07 PM
dcjmrPOLYML201979c83114: The byte offset to the flags byte depends on whether this is big- or little…Sat, May 15, 1:07 PM
makariusrISABELLE3ab18af9b2b5: clarified signature;Sat, May 15, 12:33 PM
makariusrISABELLE8444d4ff5646: clarified log content;Sat, May 15, 12:25 PM
makariusrISABELLE2f9877db82a1: reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool…Fri, May 14, 9:32 PM
paulson <lp15@cam.ac.uk>rAFPe93051f65b1a: strict_sorted now an abbreviation
paulson <lp15@cam.ac.uk> committed rAFPe93051f65b1a: strict_sorted now an abbreviation. 
Fri, May 14, 4:48 PM
paulson <lp15@cam.ac.uk>rISABELLE60a788467639: strict_sorted now an abbreviation
paulson <lp15@cam.ac.uk> committed rISABELLE60a788467639: strict_sorted now an abbreviation. 
Fri, May 14, 1:43 PM
dcjmrPOLYMLb928d20ac26f: Fix incorrect function names.Fri, May 14, 1:15 PM
dcjmrPOLYML24a06d603b74: Remove the test of GC in a forked child. This seems to fail badly on some…Fri, May 14, 9:40 AM
dcjmrPOLYMLaac4d1e94ad0: Replace usleep with nanosleep. Posix defines usleep to work only for values of…Fri, May 14, 9:16 AM
dcjmrPOLYML0e446f3e042c: Use shadow area if necessary when setting ARM relocations.Thu, May 13, 9:11 PM
paulsonrAFP41cc428000e3: merged
paulson committed rAFP41cc428000e3: merged. 
Thu, May 13, 6:32 PM
paulson <lp15@cam.ac.uk>rAFPa757f7e7c954: deleted needless material
paulson <lp15@cam.ac.uk> committed rAFPa757f7e7c954: deleted needless material. 
Thu, May 13, 6:31 PM
dcjmrPOLYMLc73509f16f52: Fix byte offset to flags in big-endian mode. The value in 201979c8 was wrong.Thu, May 13, 4:55 PM
makariusrISABELLE9267a04aabe6: tuned;Thu, May 13, 3:52 PM
makariusrISABELLEcaa5a257d3ed: unused;Thu, May 13, 3:38 PM
dcjmrPOLYMLde553b7fde0a: Fix incorrect mask in 8ee44e4.Thu, May 13, 3:04 PM
dcjmrPOLYML1a29bb7f55dd: Change argument type so that it is compatible with big-endian 32-in-64.Thu, May 13, 2:50 PM
dcjmrPOLYML8ee44e4270dc: Fix longWordToTagged for big-endian 32-in-64.Thu, May 13, 2:14 PM
dcjmrPOLYML2dc15cf77976: Fix interpreter after RTS function change.Thu, May 13, 12:49 PM
paulson <lp15@cam.ac.uk>rAFP8ff1ebba38da: more small simplifications
paulson <lp15@cam.ac.uk> committed rAFP8ff1ebba38da: more small simplifications. 
Wed, May 12, 11:20 PM
florian.haftmannrAFPa055a33fcb58: next step to phase out ancient numeralsWed, May 12, 7:05 PM
florian.haftmannrAFPa19043a5f828: explicit type class operations for type-specific implementationsWed, May 12, 7:05 PM
florian.haftmannrISABELLE78044b2f001c: explicit type class operations for type-specific implementationsWed, May 12, 7:05 PM
florian.haftmannrISABELLE3708884bfa8a: obsoleteWed, May 12, 7:05 PM
makariusrISABELLE8c4ba5f61223: unused (see 8ffc607c345d);Wed, May 12, 5:17 PM
makariusrISABELLE54fe8cc0e1c6: clarified signature: provide access to previous state;Wed, May 12, 4:47 PM
dcjmrPOLYML18716c3f4dab: Fixes to Unix files after RTS function change.Wed, May 12, 3:30 PM
dcjmrPOLYML4aa7a6f54fc0: Change argument types of RTS functions so that they are always POLYUNSIGNED…Wed, May 12, 3:17 PM
makariusrISABELLEb9aae426e51d: clarified signature (see Scala version);Wed, May 12, 2:55 PM
makariusrISABELLEc17253cad5c6: tuned signature;Wed, May 12, 1:10 PM
dcjmrPOLYMLed789f849841: Fix name change omitted when this was last committed.Wed, May 12, 1:08 PM
dcjmrPOLYML601c48c6ad68: Updated 32-bit bootstrap file with support for big-endian.Wed, May 12, 12:49 PM
makariusrISABELLEa63d76ba0a03: avoid duplicate loading of ML file;Wed, May 12, 12:22 PM
desharnarISABELLE50437744eb1c: added lemmas map_ran_Cons_sel and (length|map_fst)_map_ranWed, May 12, 9:31 AM
nipkowrISABELLE71c45d60a90a: merged
nipkow committed rISABELLE71c45d60a90a: merged. 
Wed, May 12, 6:35 AM
nipkowrISABELLE78929c029785: generalized typeTue, May 11, 10:40 PM
makariusrISABELLE73c50ce808ed: basic setup of Isabelle setup tool --- pure Java, no dependencies;Tue, May 11, 9:57 PM
makariusrISABELLE51429b78aadf: mergedTue, May 11, 9:21 PM
makariusrISABELLE6c56f2ebe157: guess package more directly;Tue, May 11, 8:19 PM
paulsonrAFP26d8da1ea081: merged
paulson committed rAFP26d8da1ea081: merged. 
Tue, May 11, 7:59 PM
paulson <lp15@cam.ac.uk>rAFPb383e59aa162: fixed some latex; tried the alternative definition of RamseyTue, May 11, 7:59 PM
paulsonrISABELLE0d79ac2eb106: merged
paulson committed rISABELLE0d79ac2eb106: merged. 
Tue, May 11, 7:56 PM
dcjmrPOLYMLa182946ad8e3: Have to take account of endian-ness when clearing ADR/LDR instruction offsets.Tue, May 11, 6:18 PM
makariusrISABELLE70d3c7009a65: proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;Tue, May 11, 4:55 PM
paulson <lp15@cam.ac.uk>rISABELLEedb01b64dc16: Just one lemma
paulson <lp15@cam.ac.uk> committed rISABELLEedb01b64dc16: Just one lemma. 
Tue, May 11, 4:50 PM
makariusrISABELLE7404f2e1d092: clarified platforms;Tue, May 11, 4:30 PM
dcjmrPOLYMLf2c0c9e261cd: Convert instruction values to little-endian when converting to ADRP/LDR.Tue, May 11, 3:59 PM
dcjmrPOLYMLfae25684e69e: Register mask is in an instruction and needs to be converted on big-endian.Tue, May 11, 2:47 PM
makariusrISABELLEff716ecb0805: put more resources into jedit_build component;Tue, May 11, 2:29 PM
makariusrISABELLE02351b514b34: proper jEdit.props (amending ff716ecb0805);Tue, May 11, 2:29 PM
makariusrISABELLE4121fc47432b: mergedTue, May 11, 2:04 PM
makariusrISABELLE02351b514b34: proper jEdit.props (amending ff716ecb0805);Tue, May 11, 2:03 PM
makariusrISABELLE5e12dad8d09b: update to gmp-6.2.1, with support for arm64-darwin;Tue, May 11, 1:45 PM
dcjmrPOLYML201979c83114: The byte offset to the flags byte depends on whether this is big- or little…Tue, May 11, 1:20 PM
makariusrISABELLE442460fba2a4: clarified platforms;Tue, May 11, 1:06 PM
makariusrISABELLE4d0df84a5b88: clarified options: implicitly support both x86_64 and arm64;Tue, May 11, 12:21 PM
dcjmrPOLYMLf2dce0a9fbd2: Constants and offsets need to be big-endian on big-endian architecture.Tue, May 11, 12:15 PM
makariusrISABELLE9ab1d5fa84d0: tuned whitespace;Tue, May 11, 11:17 AM
dcjmrPOLYML3f9b811f7c37: Convert between little-endian instruction format and native word.Tue, May 11, 9:52 AM
dcjmrPOLYML919fbd7d0a28: Support for NetBSD elf file. Work-around for misnamed(?) relocation symbol in…Tue, May 11, 9:22 AM
dcjmrPOLYMLdd4456fbd346: Updated bootstrap file for 64-bits with support for big-endian.Tue, May 11, 9:14 AM
makariusrISABELLE8b3e672df28c: proper build for fresh target directory (amending d9823224fcfe);Mon, May 10, 10:58 PM
makariusrISABELLEd9823224fcfe: build auxiliary jEdit component in Isabelle/Scala;Mon, May 10, 10:58 PM
makariusrISABELLEf6b453449cc6: more brackets;Mon, May 10, 10:58 PM
makariusrISABELLEaf82097b4adc: more brackets (see f6b453449cc6);Mon, May 10, 10:58 PM
makariusrISABELLE8b3e672df28c: proper build for fresh target directory (amending d9823224fcfe);Mon, May 10, 10:32 PM
makariusrISABELLEff716ecb0805: put more resources into jedit_build component;Mon, May 10, 10:18 PM
florian.haftmannrAFP0ace227c4d10: centralized more lemmasMon, May 10, 9:46 PM
florian.haftmannrISABELLE6e26d06b24b1: centralized more lemmasMon, May 10, 9:46 PM
florian.haftmannrAFPaac14245270a: avoid Fun.swapMon, May 10, 9:45 PM
florian.haftmannrISABELLE7734c442802f: avoid Fun.swapMon, May 10, 9:45 PM
florian.haftmannrAFP3945ab3f00b8: guide is out of focusMon, May 10, 9:45 PM
florian.haftmannrISABELLEfecfb96474ca: guide is out of focusMon, May 10, 9:45 PM
paulson <lp15@cam.ac.uk>rAFP9340467e8c9a: Trying out Ramsey_eq for simpler proofs
paulson <lp15@cam.ac.uk> committed rAFP9340467e8c9a: Trying out Ramsey_eq for simpler proofs. 
Mon, May 10, 9:45 PM
makariusrISABELLEaf82097b4adc: more brackets (see f6b453449cc6);Mon, May 10, 8:09 PM
dcjmrPOLYMLf5dd6093d760: Merge branch 'master' into ARM64TestingMon, May 10, 6:58 PM
makariusrISABELLEf6b453449cc6: more brackets;Mon, May 10, 6:31 PM
makariusrISABELLE6e85281177df: proper condition: z3 could be absent, e.g. on arm64-linux;Mon, May 10, 5:35 PM
makariusrISABELLEdceb5dde442f: proper settings variable, amending 6e85281177df;Mon, May 10, 5:35 PM
makariusrISABELLEdceb5dde442f: proper settings variable, amending 6e85281177df;Mon, May 10, 5:15 PM
makariusrISABELLEd5c3eee7da74: separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597);Mon, May 10, 5:14 PM