Diffusion afp-devel 26adfcf755e4

merged
26adfcf755e4
Actions

Description

merged

Details

Provenance

paulson

Authored on

Parents

rAFP4b812a85fec9: Purely cosmetic
rAFPac12d61f247c: added missing congruence rule

Branches

Unknown

Tags

Unknown

Event Timeline

paulson committed rAFP26adfcf755e4: merged.Sep 13 2022, 5:27 PM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

ac12d61f247c added missing congruence rule
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
34a31d29f666 streamlined
Author
florian.haftmann
Browse Repository
No Builds
No Audits
88472837e524 tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious…
Author
makarius
Browse Repository
No Builds
No Audits
4fc8e413c764 tuned whitespace;
Author
makarius
Browse Repository
No Builds
No Audits
371a56964189 merged
Author
Christian Urban <christian.urban@kcl.ac.uk>
Browse Repository
No Builds
No Audits
bd51aaa8a192 some slight polishing in the UTM entry
Author
Christian Urban <christian.urban@kcl.ac.uk>
Browse Repository
No Builds
No Audits
917f3041ca30 added congruence rule for forallM of Error-Monad
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
d90ff1d6d4ab updated to devel
Author
nipkow
Browse Repository
No Builds
No Audits
bf6ee51dd702 merged
Author
makarius
Browse Repository
No Builds
No Audits
a0b37d38544b tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious…
Author
makarius
Browse Repository
No Builds
No Audits
4345ca3dd26c removed obsolete workaround (see Isabelle/91ee232b4211);
Author
makarius
Browse Repository
No Builds
No Audits
4bdd34701622 Eliminated the temporary material that was already migrated to the Isabelle…
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
2752cd0567c9 merge from afp-2021-1
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
2011079530c4 regenerate site;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
6d58e998e657 tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
72772a622eb3 merged
Author
paulson
Browse Repository
No Builds
No Audits
11a3d3871dea New entry CRYSTALS-Kyber
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
afc81491665d regenerate site;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
791a909ac26e added missing history in metadata;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
ac2b59b37741 retrieve missing change history in metadata migration tool;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
490d1fdcd266 backout b2ae7c2c3ea51af8f43b76cdcb5d499c5085e726
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
457e3b13987e new email address for Maksym
Author
kleing
Browse Repository
No Builds
No Audits
e91943d681a1 metadata and sitegen for Khovansikii_Theorem
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
c91e67482c60 new entry: Khovanski-Theorem
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
4b1af6f3fd24 fixed metadata for Hales_Jewett
Author
pruvisto
Browse Repository
No Builds
No Audits
7a3ce4a5cdf8 sitegen for Number_Theoretic_Transform
Author
pruvisto
Browse Repository
No Builds
No Audits
9480bd426471 new entry Number_Theoretic_Transform
Author
pruvisto
Browse Repository
No Builds
No Audits
a236359e9eb6 new entry Hales Jewett
Author
nipkow
Browse Repository
No Builds
No Audits
17b82e6796f6 adapt to only check ROOT for directories in thys (aftermath of…
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
4b29df4907c3 close
Author
kleing
Browse Repository
No Builds
No Audits
eff9d8ce7be8 merge closed heads
Author
kleing
Browse Repository
No Builds
No Audits
3845c7c84c17 merged via grafting
Author
kleing
Browse Repository
No Builds
No Audits
23f824709665 merged via afp-2021-1
Author
kleing
Browse Repository
No Builds
No Audits
450bdc5c8df0 updated afp sitegen doc;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
b0bf102f7744 replaced python afp stats with Isabelle/Scala tool;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
5f4c73b43f60 updated afp metadata doc (now as markdown);
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
3cf91dd7a995 afp components: removed unnecessary platforms;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
f7b9b71b4184 afp sitegen: switch to new version;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8e3c06373cdb add sitegen ignore option;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8c4802ca1952 improvements for toml module: proper boolean values;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
7b2fbe17e4f0 add components as proper afp deps;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8e081a5e444f tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
882923327135 switched to standalone cross-platform afp python component;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
b88f372899cd tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9e91b75d851a afp python build: use tgz for better cross-plattform compatability;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8fd101fe8fd2 replaced ci_profiles by statically compiled afp_build tool (Scala 3…
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
27fff681c7f2 afp structure: added accessors;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
860c2dbfbd78 hugo site: minor changes;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
4e300068e651 merged
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
f4ad2145b146 hugo-site: improve various aspects;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits

Changes (3)

Path

Size

thys/

Ackermanns_not_PR/

Primrec.thy

Roth_Arithmetic_Progressions/

Roth_Arithmetic_Progressions.thy

Wetzels_Problem/

Wetzels_Problem.thy

rAFP26adfcf755e4

View Options

thys/Ackermanns_not_PR/Primrec.thy

View Options

thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy

View Options

thys/Wetzels_Problem/Wetzels_Problem.thy

merged26adfcf755e4Actions

Description

Details

Event Timeline

Merged Changes

Changes (3)

rAFP26adfcf755e4

thys/Ackermanns_not_PR/Primrec.thy

thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy

thys/Wetzels_Problem/Wetzels_Problem.thy

merged
26adfcf755e4
Actions