Changes from Mercurial (hg https://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- merged
- suppress arm64-darwin, which does not support "-codegen native" (required for AFP/PAC_Checker); clarified NEWS;
- update to sumatra_pdf-3.5.2;
- tuned signature: fewer warnings in IntelliJ IDEA;
- update to jsoup-1.17.2;
- proper bib entries (amending 82aaa0d8fc3b);
- update to dotnet-8.0.203;
- enforce rebuild of Isabelle/ML;
- update to sqlite-3.45.2.0: clarified component name, following postgresql;
- activate postgresql-42.7.3;
- update to postgresql-42.7.3; clarified component directory;
- update to mlton-20210117-2, which covers x86_64-linux, x86_64-darwin, arm64-darwin;
- isabelle update -u cite;
- raise error if benchmarking fails;
- option for benchmark session;
- add hosts option to run benchmark on the cluster from the command-line;
- only start jobs early if they are due (cf. 1966578feff8);
- New material from a variety of sources (including AFP)
Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)
Summary
- Patching some proofs, for of_nat_int_ceiling
- Deletion of material that had been moved to the distribution
The file was modified | thys/Amortized_Complexity/Amortized_Examples.thy |
The file was modified | thys/Amortized_Complexity/Amortized_Framework0.thy |
The file was modified | thys/Expander_Graphs/Expander_Graphs_Strongly_Explicit.thy |
The file was modified | thys/Frequency_Moments/Frequency_Moment_2.thy |
The file was modified | thys/Median_Of_Medians_Selection/Median_Of_Medians_Selection.thy |
The file was modified | thys/Root_Balanced_Tree/Root_Balanced_Tree.thy |
The file was modified | thys/Amicable_Numbers/Amicable_Numbers.thy |
The file was modified | thys/DiscretePricing/Fair_Price.thy |
The file was modified | thys/Polylog/Polylog_Library.thy |