Diffusion afp-devel 8ed602cdcb58

Merge
8ed602cdcb58
Actions

Description

Merge

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rAFP50da79b217bc: Tidied (a lot)
rAFP9839b66f7c66: merged

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rAFP8ed602cdcb58: Merge.Aug 31 2022, 12:24 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
9e2b85708f73 updated entry for Universal Turing Machines
Author
Christian Urban <christian.urban@kcl.ac.uk>
Browse Repository
No Builds
No Audits
da1092b22903 merged
Author
desharna
Browse Repository
No Builds
No Audits
13d7491c6ab9 adapted to antimono
Author
desharna
Browse Repository
No Builds
No Audits
12747ed77d71 merged
Author
desharna
Browse Repository
No Builds
No Audits
64d28014cec0 adapted to new mono and strict_mono
Author
desharna
Browse Repository
No Builds
No Audits
17f4fbb45f9c updated to Isabelle/5ea588440b06
Author
desharna
Browse Repository
No Builds
No Audits
ff719c05809a Updated citations
Author
Thibault Dardinier <thibault.dardinier@inf.ethz.ch>
Browse Repository
No Builds
No Audits
73f15452e56f Updated citations
Author
Thibault Dardinier <thibault.dardinier@inf.ethz.ch>
Browse Repository
No Builds
No Audits
6c87f24bb773 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
14eb275d680e merged
Author
Christian Urban <christian.urban@kcl.ac.uk>
Browse Repository
No Builds
No Audits
f294e5dddd66 Substantial additions by Franz Regensburger to the Universal_Turing_Machine…
Author
Christian Urban <christian.urban@kcl.ac.uk>
Browse Repository
No Builds
No Audits
5a1267ab6b71 tuned timeouts, based on test runs with threads=1;
Author
makarius
Browse Repository
No Builds
No Audits
10120a93e155 replaced slow smt call by blast
Author
blanchette
Browse Repository
No Builds
No Audits
337819a49c4b avoid hardwired document;
Author
makarius
Browse Repository
No Builds
No Audits
9839b66f7c66 merged
Author
paulson
Browse Repository
No Builds
No Audits
4ba03d4cf30e cosmetic
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
ad3c436a878d replace smt_oracle by proper veriT reconstruction
Author
mathias.fleury
Browse Repository
No Builds
No Audits
15d285a97ae0 merged
Author
paulson
Browse Repository
No Builds
No Audits
a3d1b4509a4d tweaks
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
64cf94d5181c make all sessions of chapter "AFP" belong to group "AFP";
Author
makarius
Browse Repository
No Builds
No Audits
349b20f17308 chapter_definition for presentation;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (1)

Path

Size

thys/

Ackermanns_not_PR/

Primrec.thy

rAFP8ed602cdcb58

View Options

thys/Ackermanns_not_PR/Primrec.thy

Merge8ed602cdcb58Actions

Description

Details

Event Timeline

Merged Changes

Changes (1)

rAFP8ed602cdcb58

thys/Ackermanns_not_PR/Primrec.thy

Merge
8ed602cdcb58
Actions