Page MenuHomeIsabelle/Phabricator
Feed All Stories

Today

Fabian Huch <huch@in.tum.de> committed rAFP7a425b5f62ba: tuned: prefer for-comprehension in complicated situations;.
tuned: prefer for-comprehension in complicated situations;
Thu, Mar 28, 6:51 PM
Fabian Huch <huch@in.tum.de> committed rAFP01987db5d362: tuned: more uniform Isabelle style;.
tuned: more uniform Isabelle style;
Thu, Mar 28, 6:50 PM
Fabian Huch <huch@in.tum.de> committed rAFPb93b79b9240e: tuned formatting;.
tuned formatting;
Thu, Mar 28, 6:50 PM
Fabian Huch <huch@in.tum.de> committed rAFPb7690d847464: tuned;.
tuned;
Thu, Mar 28, 6:50 PM
Fabian Huch <huch@in.tum.de> committed rAFPf111b9c197e8: tuned imports;.
tuned imports;
Thu, Mar 28, 6:50 PM
Fabian Huch <huch@in.tum.de> committed rAFP307a818fb212: clarified options;.
clarified options;
Thu, Mar 28, 6:50 PM
Emin Karayel <me@eminkarayel.de> committed rAFPf8eca525e197: Distributed_Distinct_Elements: Fix aliasing issue introduce in isabelle….
Distributed_Distinct_Elements: Fix aliasing issue introduce in isabelle…
Thu, Mar 28, 6:14 PM
makarius committed rAFP0df87a34e8a0: merged.
merged
Thu, Mar 28, 5:51 PM
makarius committed rAFPabe7b3319f06: tuned whitespace;.
tuned whitespace;
Thu, Mar 28, 5:51 PM
makarius committed rAFP5aca58481bd5: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Thu, Mar 28, 5:51 PM
makarius committed rAFP2c25484e1496: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Thu, Mar 28, 5:51 PM
makarius committed rAFP4c396108a3a9: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Thu, Mar 28, 5:51 PM
Fabian Huch <huch@in.tum.de> committed rAFP4cb970a0955a: clarified types: richer interface for metadata;.
clarified types: richer interface for metadata;
Thu, Mar 28, 5:21 PM
Fabian Huch <huch@in.tum.de> committed rAFP9cad40069322: add option to run formatting operations on all metadata files;.
add option to run formatting operations on all metadata files;
Thu, Mar 28, 5:21 PM
Fabian Huch <huch@in.tum.de> committed rAFP4395ecd3d7a5: tuned;.
tuned;
Thu, Mar 28, 5:21 PM
Fabian Huch <huch@in.tum.de> committed rAFPcefde457b8cc: tuned;.
tuned;
Thu, Mar 28, 5:21 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE68f6b29ae066: tuned;.
tuned;
Thu, Mar 28, 5:19 PM
makarius committed rISABELLE87f90735e6dd: removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g..
removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g.
Thu, Mar 28, 4:45 PM
makarius committed rISABELLE9279e96eb34e: clarified signature;.
clarified signature;
Thu, Mar 28, 4:45 PM
makarius committed rISABELLE42bc8ab751c1: clarified modules: more official Sessions.notable_groups;.
clarified modules: more official Sessions.notable_groups;
Thu, Mar 28, 4:45 PM
makarius committed rAFP9ce4d6a809c6: update to Isabelle/42bc8ab751c1;.
update to Isabelle/42bc8ab751c1;
Thu, Mar 28, 4:45 PM
nipkow committed rISABELLEf8d7df38d7c6: tuned.
tuned
Thu, Mar 28, 4:16 PM
paulson committed rISABELLE44d8fb3da9d5: merged.
merged
Thu, Mar 28, 2:33 PM
paulson <lp15@cam.ac.uk> committed rISABELLE35b2143aeec6: An assortment of new material, mostly due to Manuel.
An assortment of new material, mostly due to Manuel
Thu, Mar 28, 2:33 PM
makarius committed rISABELLE9cdc4f533b91: rebuild rsync-3.2.7 on current platforms, including native arm64-darwin;.
rebuild rsync-3.2.7 on current platforms, including native arm64-darwin;
Thu, Mar 28, 1:16 PM
makarius committed rISABELLE7d8a24c5559d: tuned signature;.
tuned signature;
Thu, Mar 28, 12:20 PM
makarius committed rISABELLEb525f783b784: tuned;.
tuned;
Thu, Mar 28, 12:20 PM
makarius committed rISABELLEa213dd3c0b29: tuned signature;.
tuned signature;
Thu, Mar 28, 12:19 PM
desharna committed rISABELLE38803a6b3357: added lemma wfp_on_image and author name to theory.
added lemma wfp_on_image and author name to theory
Thu, Mar 28, 8:31 AM
desharna committed rISABELLE19cc354ba625: merged.
merged
Thu, Mar 28, 8:31 AM

Yesterday

makarius committed rISABELLE308ccc1ef982: proper ISABELLE_GO_SETUP, e.g. for AFP/Go compiler tests;.
proper ISABELLE_GO_SETUP, e.g. for AFP/Go compiler tests;
Wed, Mar 27, 10:56 PM
makarius committed rAFP1699d5f4b11d: proper Go setup, following Isabelle/da323d3d7570;.
proper Go setup, following Isabelle/da323d3d7570;
Wed, Mar 27, 10:35 PM
makarius committed rISABELLEda323d3d7570: proper "isabelle go_setup" for Jenkins;.
proper "isabelle go_setup" for Jenkins;
Wed, Mar 27, 10:12 PM
makarius committed rAFP1a2512112874: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Mar 27, 9:52 PM
makarius committed rAFPd8244335636c: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Mar 27, 9:52 PM
makarius committed rAFPd9d45697c125: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Mar 27, 9:52 PM
makarius committed rAFP455b44957816: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Mar 27, 9:52 PM
makarius committed rAFPd0bd37a0fea4: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Mar 27, 9:52 PM
makarius committed rISABELLEa0210a24b547: dummy Admin/components/go to avoid crash of Jenkins (see 38bbc2ff3c24);.
dummy Admin/components/go to avoid crash of Jenkins (see 38bbc2ff3c24);
Wed, Mar 27, 9:51 PM
makarius committed rISABELLE742e39db4d58: tuned message;.
tuned message;
Wed, Mar 27, 5:51 PM
makarius committed rISABELLEa0f93621c332: merged.
merged
Wed, Mar 27, 5:47 PM
makarius committed rISABELLE30eb547bda4a: tuned NEWS;.
tuned NEWS;
Wed, Mar 27, 5:47 PM
makarius committed rISABELLE0732ee5c8ee1: support for "all" platforms;.
support for "all" platforms;
Wed, Mar 27, 5:47 PM
makarius committed rISABELLEb1e2246147eb: clarified signature;.
clarified signature;
Wed, Mar 27, 5:47 PM
nipkow committed rAFPbd6e0a8eeb23: updates to new time function generator that now translates undefined to….
updates to new time function generator that now translates undefined to…
Wed, Mar 27, 5:11 PM
nipkow committed rISABELLE9b2f72f5a29a: merged.
merged
Wed, Mar 27, 4:48 PM
nipkow committed rISABELLEa594d22e69d6: updated time functions for Array_Braun.
updated time functions for Array_Braun
Wed, Mar 27, 4:48 PM
paulson <lp15@cam.ac.uk> committed rAFP18437ad04fb8: Fixes mostly for log_mono aliasing.
Fixes mostly for log_mono aliasing
Wed, Mar 27, 4:18 PM
paulson <lp15@cam.ac.uk> committed rISABELLE95b4fb2b5359: New material and a bit of refactoring.
New material and a bit of refactoring
Wed, Mar 27, 4:17 PM
paulson committed rISABELLEc964cd759f47: merged.
merged
Wed, Mar 27, 4:17 PM
makarius committed rISABELLE71d005ffa9fe: remove unused TEMP_WINDOWS more thoroughly (see also fa18208fd7bd and….
remove unused TEMP_WINDOWS more thoroughly (see also fa18208fd7bd and…
Wed, Mar 27, 3:53 PM
makarius committed rISABELLE98808cc7b0c1: tuned;.
tuned;
Wed, Mar 27, 3:02 PM
makarius committed rISABELLEebd988ee1d57: more robust Markdown;.
more robust Markdown;
Wed, Mar 27, 2:40 PM
makarius committed rISABELLE5c00c04f09fb: misc tuning;.
misc tuning;
Wed, Mar 27, 2:39 PM
makarius committed rISABELLEa2d15ad6877a: run "isabelle components_build -u";.
run "isabelle components_build -u";
Wed, Mar 27, 2:20 PM
makarius committed rISABELLE38bbc2ff3c24: remove obsolete component (see 8347ffa1f92c): superseded by "isabelle go_setup";.
remove obsolete component (see 8347ffa1f92c): superseded by "isabelle go_setup";
Wed, Mar 27, 1:41 PM
makarius committed rISABELLEa03a7d4b82f8: more Setup_Tool services;.
more Setup_Tool services;
Wed, Mar 27, 1:41 PM
makarius committed rISABELLE64e57aafca1e: tuned order;.
tuned order;
Wed, Mar 27, 1:41 PM
makarius committed rISABELLE27f2a6bd5616: proper SSH operations;.
proper SSH operations;
Wed, Mar 27, 1:41 PM
makarius committed rISABELLEd1ac1bb01060: clarified signature;.
clarified signature;
Wed, Mar 27, 1:41 PM
makarius committed rISABELLE77e605c66797: clarified signature: explicit variable is easier to find in source;.
clarified signature: explicit variable is easier to find in source;
Wed, Mar 27, 1:41 PM
makarius committed rISABELLEc43a51fde4f5: tuned signature: more permissive;.
tuned signature: more permissive;
Wed, Mar 27, 1:41 PM
makarius committed rISABELLEba06861e91f9: proper services for Setup_Tool --- avoid hardwired stuff;.
proper services for Setup_Tool --- avoid hardwired stuff;
Wed, Mar 27, 1:41 PM
paulson <lp15@cam.ac.uk> committed rAFPc6e769593bac: Brought this new entry up-to-date with the development version.
Brought this new entry up-to-date with the development version
Wed, Mar 27, 12:12 PM
desharna committed rISABELLEb0a46cf73aa4: merged.
merged
Wed, Mar 27, 10:56 AM
desharna committed rISABELLE991557e01814: renamed lemma wfP_iff_ex_minimal to wfp_iff_ex_minimal.
renamed lemma wfP_iff_ex_minimal to wfp_iff_ex_minimal
Wed, Mar 27, 10:56 AM
Lars Hupel <lars@hupel.info> committed rAFP070dbf86a3c1: merged.
merged
Wed, Mar 27, 7:11 AM
paulson <lp15@cam.ac.uk> committed rAFP7e1cd1183cd3: sitegen for Continued_Fractions.
sitegen for Continued_Fractions
Wed, Mar 27, 7:11 AM
traytel committed rAFPdbea0a138a7e: sitegen for Approximate_Model_Counting.
sitegen for Approximate_Model_Counting
Wed, Mar 27, 7:11 AM
paulson <lp15@cam.ac.uk> committed rAFP83d6170644f2: New entry "Continued_Fractions".
New entry "Continued_Fractions"
Wed, Mar 27, 7:11 AM
traytel committed rAFP1bbc2988758b: tuned (removing warnings).
tuned (removing warnings)
Wed, Mar 27, 7:11 AM
traytel committed rAFP537ec6a3e46e: new entry Approximate_Model_Counting.
new entry Approximate_Model_Counting
Wed, Mar 27, 7:11 AM
peter_lammich committed rAFP5ad47a63f9ef: Go: website updates.
Go: website updates
Wed, Mar 27, 7:11 AM
peter_lammich committed rAFPaafd2b24370d: Go submission.
Go submission
Wed, Mar 27, 7:11 AM

Tue, Mar 26

makarius committed rISABELLEac4412562c7b: more robust XML body: allow empty text, as well as arbitrary pro-forma markup….
more robust XML body: allow empty text, as well as arbitrary pro-forma markup…
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEce9b649ee2dd: NEWS for "isabelle go_setup";.
NEWS for "isabelle go_setup";
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEfb96063456fd: more robust: untyped/unscoped markup elements need to reside in module Markup….
more robust: untyped/unscoped markup elements need to reside in module Markup…
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE339325fdb128: misc tuning for release;.
misc tuning for release;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE6d01661a055b: merged;.
merged;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE07c83d3369c0: misc tuning, following go_setup;.
misc tuning, following go_setup;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEf1686f71dffc: proper platform_path for Windows;.
proper platform_path for Windows;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEb082476a8036: dynamic setup of Go component, similar to Dotnet;.
dynamic setup of Go component, similar to Dotnet;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEac10e32938df: clarified signature: more operations;.
clarified signature: more operations;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE6964a23f595a: tuned comments;.
tuned comments;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE914c4a81027d: clarified signature: explicit type Platform.Info with derived operations;.
clarified signature: explicit type Platform.Info with derived operations;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEa4d94dd5c210: less ambitious parallelism: avoid exhaustion of memory (64GB total);.
less ambitious parallelism: avoid exhaustion of memory (64GB total);
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE34c20c8bbdc5: tuned;.
tuned;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEd89685d3d306: provide ISABELLE_DOTNET_VERSION via settings, following "isabelle ghc_setup";.
provide ISABELLE_DOTNET_VERSION via settings, following "isabelle ghc_setup";
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE31ebb6be32b0: tuned messages;.
tuned messages;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE7e52091795e8: update to bash_process-20240326;.
update to bash_process-20240326;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEee449ca91c3b: build bash_process in Isabelle/Scala, with etc/platforms.prop to preserve all….
build bash_process in Isabelle/Scala, with etc/platforms.prop to preserve all…
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE98384596b54b: clarified meaning of platform.props: update on default;.
clarified meaning of platform.props: update on default;
Tue, Mar 26, 10:12 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE11a1f4d7af51: allow raw input in HTML (e.g., for web applications);.
allow raw input in HTML (e.g., for web applications);
Tue, Mar 26, 4:07 PM
Fabian Huch <huch@in.tum.de> committed rAFPba52e1ff7569: adapt to Isabelle/11a1f4d7af51;.
adapt to Isabelle/11a1f4d7af51;
Tue, Mar 26, 4:07 PM
Fabian Huch <huch@in.tum.de> committed rAFPa10b74bad3f1: use emph instead of italic;.
use emph instead of italic;
Tue, Mar 26, 4:07 PM
Fabian Huch <huch@in.tum.de> committed rAFP7b3ccda1eee6: tuned;.
tuned;
Tue, Mar 26, 4:07 PM
Fabian Huch <huch@in.tum.de> committed rAFPab8dd4efb9fb: clarified names;.
clarified names;
Tue, Mar 26, 4:07 PM
desharna committed rISABELLEdca9c237d108: added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and….
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and…
Tue, Mar 26, 3:44 PM
desharna committed rAFP74a3f7ca4640: tuned lemmas.
tuned lemmas
Tue, Mar 26, 10:18 AM
desharna committed rAFPed7c8d390745: merged.
merged
Tue, Mar 26, 9:58 AM