Diffusion afp-devel 7c831b848ada

merge from afp-2021
7c831b848ada
Actions

Description

merge from afp-2021

Details

Provenance

kleing

Authored on

Parents

rAFP6d3ed174962a: document `publish -`
rAFP727a899b0f44: tuned proofs -- avoid z3;

Branches

Unknown

Tags

Unknown

Event Timeline

kleing committed rAFP7c831b848ada: merge from afp-2021.Nov 14 2021, 4:09 AM

Merged Changes

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

727a899b0f44 tuned proofs -- avoid z3;
Author
makarius
Browse Repository
No Builds
No Audits
3dc8035b2428 added missing topics;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
3aae61bb0567 clarified hugo build signature;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d2e0fd5a6ec2 added more steps to afp site generation tool;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
a40fc791abac tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
3e1f6e97fb35 added hugo project by Carlin MacKenzie;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
fb767a74d676 added sitegen scripts by Carlin MacKenzie (slightly tweaked);
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9895c8d9135b added afp hugo module;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
17494afe4715 clarified afp_dependencies: proper typed output;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d08381f4f088 Added afp structure module;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
2272fe40054f Added python wrapper;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
bb594d6d379d clarified metadata;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8225e73dbf62 tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
153b52d5a513 added afp hugo component;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
22ee7f2dcda1 added afp python component with required packages;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
4f170b69e2da merged;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
061880a9cd9e feat(afp/tools): added initial site build tool
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
ead6c0ad1a67 tuned(afp/tools): metadata sorted
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
3c6fcf371feb CTR and ETTS: integration with SpecCheck
Author
user9716869 <user9716869@gmail.com>
Browse Repository
No Builds
No Audits
e5eeaaf2bd5b used antiquotation to fix LaTeX failure
Author
desharna
Browse Repository
No Builds
No Audits
5dddf1525788 adapted to devel
Author
nipkow
Browse Repository
No Builds
No Audits
5270bd68a568 updated to devel
Author
nipkow
Browse Repository
No Builds
No Audits
1b4394a8fc94 merged
Author
nipkow
Browse Repository
No Builds
No Audits
0d88eeb67408 tuned proof for devel
Author
nipkow
Browse Repository
No Builds
No Audits
66a042f96686 clarified quotes vs. apostrophes vs. primes;
Author
makarius
Browse Repository
No Builds
No Audits
2b6d50818876 more accurate use of LaTeX ndash;
Author
makarius
Browse Repository
No Builds
No Audits
2c40cc64d4e5 prefer portable LaTeX mdash;
Author
makarius
Browse Repository
No Builds
No Audits
5d6db6d1389b tuned whitespace --- removed suspicious Unicode;
Author
makarius
Browse Repository
No Builds
No Audits
43ab95a583be proper Unix linefeeds;
Author
makarius
Browse Repository
No Builds
No Audits
0051ace7ae35 changed affiliation of eberl (this time properly)
Author
pruvisto
Browse Repository
No Builds
No Audits
fb912ad7a64c changed affiliation of eberl
Author
pruvisto
Browse Repository
No Builds
No Audits
88356e38a271 added author to Saturation_Framework_Extensions
Author
desharna
Browse Repository
No Builds
No Audits
70d3ed7fb774 derived calculus_with_standard_redundancy lemmas from…
Author
desharna
Browse Repository
No Builds
No Audits
e3898104e532 added locale calculus_with_finitary_standard_redundancy
Author
desharna
Browse Repository
No Builds
No Audits
37caa5102bec Registers:
Author
Dominique Unruh <unruh@ut.ee>
Browse Repository
No Builds
No Audits
6b07f915b460 feat(SpecCheck) add better unit tests facilities, examples and exceptions…
Author
kappelmann
Browse Repository
No Builds
No Audits
841135333654 discontinued somewhat pointless and slightly outdated document_preprocessor…
Author
makarius
Browse Repository
No Builds
No Audits
e9f74a71da1d Correctness_Algebras: increase nitpick timeout
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
c9ed46c09de9 CZH: dagger monoidal categories
Author
user9716869 <user9716869@gmail.com>
Browse Repository
No Builds
No Audits
6c0f80edb761 update it Isabelle/925b46043b84
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
b89191ec32d6 merge from afp-2021
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
fa45268f13d7 tuned(afp/tools): tuned parser/unparser
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
88ca579ca6cd feat(afp/tools): more metadata and toml conversion;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
a3eb648b93ca feat(afp/tools): added TOML lexer and parser;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d6535281a69a tuned(afp/tools): module jar locations;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
3a75f572994c Correctness_Algebras: increase session timeout
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
49f5cc27cb2e tuned signature, according to Isabelle/df12779c3ce8;
Author
makarius
Browse Repository
No Builds
No Audits
b9fadc5d34c4 feat(SpecCheck) add possibility to make builds fail on failure and extend README
Author
kappelmann
Browse Repository
No Builds
No Audits
0b1dccde39f0 added missing funding information
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
b40b44b920f5 restored theory structure for simple genericity.
Author
florian.haftmann
Browse Repository
No Builds
No Audits

Changes (41)

Path

Size

doc/

editors/

metadata/

templates/

Amicable_Numbers.html

Aristotles_Assertoric_Syllogistic.html

Complete_Non_Orders.html

Conditional_Transfer_Rule.html

Girth_Chromatic.html

Green.html

Irrational_Series_Erdos_Straus.html

Irrationality_J_Hancl.html

Octonions.html

Real_Power.html

Schutz_Spacetime.html

SpecCheck.html

Szemeredi_Regularity.html

Transcendence_Series_Hancl_Rucki.html

Types_To_Sets_Extension.html

rAFP7c831b848ada

View Options

doc/editors/web.md

View Options

metadata/metadata

View Options

metadata/templates/about.tpl

View Options

thys/ROOTS

View Options

thys/Real_Power/Log.thy

View Options

thys/Real_Power/ROOT

View Options

thys/Real_Power/RatPower.thy

View Options

thys/Real_Power/RealPower.thy

View Options

thys/Real_Power/document/root.tex

View Options

thys/Szemeredi_Regularity/ROOT

View Options

thys/Szemeredi_Regularity/Roth_Library.thy

View Options

thys/Szemeredi_Regularity/Szemeredi.thy

View Options

thys/Szemeredi_Regularity/document/root.bib

View Options

thys/Szemeredi_Regularity/document/root.tex

View Options

web/about.html

View Options

web/entries/Amicable_Numbers.html

View Options

web/entries/Aristotles_Assertoric_Syllogistic.html

View Options

web/entries/Complete_Non_Orders.html

View Options

web/entries/Conditional_Transfer_Rule.html

View Options

web/entries/Girth_Chromatic.html

View Options

web/entries/Green.html

View Options

web/entries/Irrational_Series_Erdos_Straus.html

View Options

web/entries/Irrationality_J_Hancl.html

View Options

web/entries/Octonions.html

View Options

web/entries/Real_Power.html

View Options

web/entries/Schutz_Spacetime.html

View Options

web/entries/SpecCheck.html

View Options

web/entries/Szemeredi_Regularity.html

View Options

web/entries/Transcendence_Series_Hancl_Rucki.html

View Options

web/entries/Types_To_Sets_Extension.html

View Options

web/index.html

View Options

web/rss.xml

View Options

web/statistics.html

View Options

merge from afp-20217c831b848adaActions

Description

Details

Event Timeline

Merged Changes

Changes (41)

rAFP7c831b848ada

doc/editors/web.md

metadata/metadata

metadata/templates/about.tpl

thys/ROOTS

thys/Real_Power/Log.thy

thys/Real_Power/ROOT

thys/Real_Power/RatPower.thy

thys/Real_Power/RealPower.thy

thys/Real_Power/document/root.tex

thys/Szemeredi_Regularity/ROOT

thys/Szemeredi_Regularity/Roth_Library.thy

thys/Szemeredi_Regularity/Szemeredi.thy

thys/Szemeredi_Regularity/document/root.bib

thys/Szemeredi_Regularity/document/root.tex

web/about.html

web/entries/Amicable_Numbers.html

web/entries/Aristotles_Assertoric_Syllogistic.html

web/entries/Complete_Non_Orders.html

web/entries/Conditional_Transfer_Rule.html

web/entries/Girth_Chromatic.html

web/entries/Green.html

web/entries/Irrational_Series_Erdos_Straus.html

web/entries/Irrationality_J_Hancl.html

web/entries/Octonions.html

web/entries/Real_Power.html

web/entries/Schutz_Spacetime.html

web/entries/SpecCheck.html

web/entries/Szemeredi_Regularity.html

web/entries/Transcendence_Series_Hancl_Rucki.html

web/entries/Types_To_Sets_Extension.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html

merge from afp-2021
7c831b848ada
Actions