Diffusion afp-devel cccf7f8d03c4

merged
cccf7f8d03c4
Actions

Description

merged

Details

Provenance

paulson

Authored on

Parents

rAFPbf87ecbb9af7: updated metadata
rAFP7c00f83aacff: New entry Multiset_Ordering_NPC

Branches

Unknown

Tags

Unknown

Event Timeline

paulson committed rAFPcccf7f8d03c4: merged.Apr 26 2022, 1:08 PM

Merged Changes

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

b8c4aec14ebf updated name and email address of Rose Bohrer
Author
pruvisto
Browse Repository
No Builds
No Audits
05cff0f17aaf sitegen for Clique_and_Monotone_Circuits
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
75635e4f695b new entry Clique_and_Monotone_Circuits
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
a6a2db6744be metadata and sitegen for Fisher's inequality
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
1da45ba16d3e new entry: Fisher's Inequality
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
7c00f83aacff New entry Multiset_Ordering_NPC
Author
nipkow
Browse Repository
No Builds
No Audits
0f61fdaf00bf sitegen for Frequence_Moments
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
a108597c1ee8 new entry: Frequence_Moments
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
11b4b5caf3fe metadata and sitegen for Prefix_Free_Code_Combinators
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
4895a13e16de new entry: Prefix_Free_Code_Combinators
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
a6affb2d1770 regen website (some orders are different in python3)
Author
kleing
Browse Repository
No Builds
No Audits
cac9b963c170 switch sitegen to python3
Author
kleing
Browse Repository
No Builds
No Audits
4ef570cafca9 updated name and email address of Rose Bohrer
Author
pruvisto
Browse Repository
No Builds
No Audits
6ae899d8db32 Removal of unnecessary material
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
0915660e2387 perfectly pointless streamlining
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
33748b892d11 More general definition of gcard
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
15a6b7cce9c7 refined one-loop version further
Author
nipkow
Browse Repository
No Builds
No Audits
b2708c764337 tidied up a few proofs
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c74a55e029d0 A bit of beautification
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
a2db1b041475 Yet more tidying and streamlining of graph lemmas
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
e1d9bd95d879 merged
Author
paulson
Browse Repository
No Builds
No Audits
c21393ad5ebd A few trivial changes
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
e41bea9e6760 Tweaks concerning the versions of Zhao's evolving lecture notes
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
341a9c84f553 Trying to simplify a bit more
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
19315034f82e More simplification of proofs. Removal of numeric references to Zhao.
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
0509d25eca91 tidying and simplification
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
0035a9575d15 merged
Author
paulson
Browse Repository
No Builds
No Audits
6be68200944c More purely cosmetic changes
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
509270282029 moved from AFP to distribution
Author
florian.haftmann
Browse Repository
No Builds
No Audits
cb5230a8e3a2 tuned syntax
Author
florian.haftmann
Browse Repository
No Builds
No Audits
aa4dd2422dc1 simplified some proofs and deleted quite a bit of redundant material
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
53d8551e20b5 Shorter proofs and leaner notation.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
4b39efe5aa65 Minor updates supplied by the author, mostly connected with a reference to a…
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
293f007783a1 Add a construction, using ZFC_in_HOL, of the category of small sets and…
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
c250cee7c7ad Resolve a "Duplicate constant declaration" issue that occurs with "isabelle…
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
667d48034562 avoid side effects on working copy while runnign sessions (generated code is…
Author
florian.haftmann
Browse Repository
No Builds
No Audits
ed0b6e223df1 clarified formatting, for the sake of scala3;
Author
makarius
Browse Repository
No Builds
No Audits
e7be02381c65 Deleted a few redundant lines
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
5dbca156122e Trying to beautify this, but it's still ugly
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
618a34159790 And a bit more tidying
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
6c97474bfa9c more renaming and tidying
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
de530263074c Alphabetic substitutions
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
883db7628b48 Eliminated another finiteness assumption
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
49e6d69ecb5a Removal of some needless finiteness assumptions
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
83736f4fc488 Removed a small amount of redundant material from both Szemerédi and Roth
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
42810d60fe4a merged
Author
paulson
Browse Repository
No Builds
No Audits
6718d889ebe3 tidied up a few proofs
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
387e1d863bf8 A slightly nicer proof
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
9643fdf0122b merged
Author
paulson
Browse Repository
No Builds
No Audits
c3f8c0a0e672 tidied and generalised some proofs using small_eqpoll
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits

Changes (9)

Path

Size

metadata/

rAFPcccf7f8d03c4

View Options

metadata/metadata

View Options

thys/ROOTS

View Options

thys/Sophomores_Dream/ROOT

View Options

thys/Sophomores_Dream/Sophomores_Dream.thy

View Options

thys/Sophomores_Dream/document/root.bib

View Options

thys/Sophomores_Dream/document/root.tex

mergedcccf7f8d03c4Actions

Description

Details

Event Timeline

Merged Changes

Changes (9)

rAFPcccf7f8d03c4

metadata/metadata

thys/ROOTS

thys/Sophomores_Dream/ROOT

thys/Sophomores_Dream/Sophomores_Dream.thy

thys/Sophomores_Dream/document/root.bib

thys/Sophomores_Dream/document/root.tex

merged
cccf7f8d03c4
Actions