Diffusion afp-devel 7ca6a77befba

merge from AFP 2021
7ca6a77befba
Actions

Description

merge from AFP 2021

Details

Provenance

nipkow

Authored on

Parents

rAFPdec422b384e4: New entry Fresh_Identifiers
rAFPe18a11ed5f49: cleaning up

Branches

Unknown

Tags

Unknown

Event Timeline

nipkow committed rAFP7ca6a77befba: merge from AFP 2021.Aug 18 2021, 12:24 PM

Merged Changes

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

e18a11ed5f49 cleaning up
Author
nipkow
Browse Repository
No Builds
No Audits
aea7c129bfe6 merged
Author
nipkow
Browse Repository
No Builds
No Audits
64560b22b6c9 cleaning up
Author
nipkow
Browse Repository
No Builds
No Audits
43e8d0e799d7 Update Bounded_Deducibility_Security
Author
Thomas Bauereiss <thomas@bauereiss.name>
Browse Repository
No Builds
No Audits
c7318a9475e5 tuned signature, following Isabelle/069f6b2c5a07;
Author
makarius
Browse Repository
No Builds
No Audits
34754976c5bf metadata update for MFMC_Countable
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
3c85bb52bbe6 derive rel_pmf characterization from bounded and unbounded MFMC theorem
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
ce3d74fa5ddf merged
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
e43bebc4bcb3 drop boundedness requirement for the sink
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
a471fb8c85c4 avoid global tmp file: pointless due to implicit theory export;
Author
makarius
Browse Repository
No Builds
No Audits
d8cd1583a4f6 repaired syntax
Author
florian.haftmann
Browse Repository
No Builds
No Audits
7924e625acd8 tuned signature, following Isabelle/d030b988d470;
Author
makarius
Browse Repository
No Builds
No Audits
bd6c4c7c76ec generalized gt_rat_sign_change to square-free polynomials
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
f9d3e8ed8c17 minor updates to bibliography
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
c3e0fa187981 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
d4adf5def3dd clarified abstract and concrete boolean algebras
Author
florian.haftmann
Browse Repository
No Builds
No Audits
393bd86c18ea antiquotation for bundles
Author
florian.haftmann
Browse Repository
No Builds
No Audits
13152a0c7b0c simplified hierarchy of type classes for bit operations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
da7fd1ac6b66 restored executable conversions
Author
florian.haftmann
Browse Repository
No Builds
No Audits
7f4f3900fd58 dropped junk
Author
florian.haftmann
Browse Repository
No Builds
No Audits
c341fdde0cba moved theory Bit_Operations into Main corpus
Author
florian.haftmann
Browse Repository
No Builds
No Audits
fc03e8f2954c organize syntax for word operations in bundles
Author
florian.haftmann
Browse Repository
No Builds
No Audits
82cfa5e04c85 more systematic approach for instantiation
Author
florian.haftmann
Browse Repository
No Builds
No Audits
f5bee47345aa avoid seemingly unused transfer rules
Author
florian.haftmann
Browse Repository
No Builds
No Audits
6beec57f7d3f cleaner presentation of analysis theorems in preliminaries
Author
yonoteam
Browse Repository
No Builds
No Audits
e1046d8be835 Update to new Epistemic_Logic.thy
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
09d0f0e8b5f5 Avoid typedefs
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
d4dfaca0753b Clean: set AFP standard document options
Author
kleing
Browse Repository
No Builds
No Audits
f775ffffa43c Clean: re-add to chapter AFP
Author
kleing
Browse Repository
No Builds
No Audits
3ccdf21c5bb4 merge from afp-2021
Author
kleing
Browse Repository
No Builds
No Audits
fdc94d7251ed Added Finitely_Generated_Abelian_Groups to metadata
Author
pruvisto
Browse Repository
No Builds
No Audits
49d3aa43c180 Sync with my development repo. Add new material: "concrete bicategories" and
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
11e377bef9e9 compile
Author
blanchette
Browse Repository
No Builds
No Audits
c6645d183e9b more realistic timeout: 50min CPU time;
Author
makarius
Browse Repository
No Builds
No Audits
1001c0dfced0 Minor changes to Finitely_Generated_Abelian_Groups, simplified and extended…
Author
Joseph Thommes <joseph-thommes@gmx.de>
Browse Repository
No Builds
No Audits
e37ae457c15a new entry Finitely_Generated_Abelian_Groups
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
aea1cfc63762 remove duplicate entry in metadata
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
1ed4c9f5c24d more coherent dependencies
Author
florian.haftmann
Browse Repository
No Builds
No Audits
44953ff0d822 fix(Regex_Equivalence) update to new SpecCheck version
Author
kappelmann
Browse Repository
No Builds
No Audits
d77834415899 operations for symbolic computation of bit operations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
835c58e469d3 fixed Proof_Strategy_Language following Isabelle/f58108b7a60c
Author
desharna
Browse Repository
No Builds
No Audits
e7547e409434 SpecCheck now without _ (Regex_Equivalence is still broken)
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
a8a03d5e5117 T1 fontenc for new entries
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
2992e460f579 sitegen
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
1c2e8c2011c9 update hide_lams -> opaque_lifting
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
a60ccd2e9cc6 merged from afp2021
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
fe45d0404b6b Removal of unintended files
Author
Susannah Mansky <susannahej@gmail.com>
Browse Repository
No Builds
No Audits
6de5937fcbcb Hidden.thy to Isar
Author
Susannah Mansky <susannahej@gmail.com>
Browse Repository
No Builds
No Audits
a3060bc70b44 merged
Author
desharna
Browse Repository
No Builds
No Audits
975b2b1d8a19 renamed hide_lams opaque_lifting
Author
desharna
Browse Repository
No Builds
No Audits

Changes (41)

Path

Size

metadata/

Aggregation_Algebras.html

Bounded_Deducibility_Security.html

Dirichlet_L.html

Finitely_Generated_Abelian_Groups.html

Fresh_Identifiers.html

KAD.html

MFMC_Countable.html

Regex_Equivalence.html

Relational_Disjoint_Set_Forests.html

Relational_Forests.html

Relational_Minimum_Spanning_Trees.html

Relational_Paths.html

SpecCheck.html

Stone_Algebras.html

Stone_Kleene_Relation_Algebras.html

Stone_Relation_Algebras.html

Subset_Boolean_Algebras.html

rAFP7ca6a77befba

View Options

metadata/metadata

View Options

thys/Fresh_Identifiers/Fresh.thy

View Options

thys/Fresh_Identifiers/Fresh_Infinite.thy

View Options

thys/Fresh_Identifiers/Fresh_Nat.thy

View Options

thys/Fresh_Identifiers/Fresh_String.thy

View Options

thys/Fresh_Identifiers/ROOT

View Options

thys/Fresh_Identifiers/document/root.tex

View Options

thys/ROOTS

View Options

thys/Relational_Forests/Algorithms.thy

View Options

thys/Relational_Forests/Forests.thy

View Options

thys/Relational_Forests/ROOT

View Options

thys/Relational_Forests/document/root.bib

View Options

thys/Relational_Forests/document/root.tex

View Options

web/entries/Aggregation_Algebras.html

View Options

web/entries/Bounded_Deducibility_Security.html

View Options

web/entries/Dirichlet_L.html

View Options

web/entries/Finitely_Generated_Abelian_Groups.html

View Options

web/entries/Fresh_Identifiers.html

View Options

web/entries/KAD.html

View Options

web/entries/MFMC_Countable.html

View Options

web/entries/Regex_Equivalence.html

View Options

web/entries/Relational_Disjoint_Set_Forests.html

View Options

web/entries/Relational_Forests.html

View Options

web/entries/Relational_Minimum_Spanning_Trees.html

View Options

web/entries/Relational_Paths.html

View Options

web/entries/SpecCheck.html

View Options

web/entries/Stone_Algebras.html

View Options

web/entries/Stone_Kleene_Relation_Algebras.html

View Options

web/entries/Stone_Relation_Algebras.html

View Options

web/entries/Subset_Boolean_Algebras.html

View Options

web/index.html

View Options

web/rss.xml

View Options

web/statistics.html

View Options

merge from AFP 20217ca6a77befbaActions

Description

Details

Event Timeline

Merged Changes

Changes (41)

rAFP7ca6a77befba

metadata/metadata

thys/Fresh_Identifiers/Fresh.thy

thys/Fresh_Identifiers/Fresh_Infinite.thy

thys/Fresh_Identifiers/Fresh_Nat.thy

thys/Fresh_Identifiers/Fresh_String.thy

thys/Fresh_Identifiers/ROOT

thys/Fresh_Identifiers/document/root.tex

thys/ROOTS

thys/Relational_Forests/Algorithms.thy

thys/Relational_Forests/Forests.thy

thys/Relational_Forests/ROOT

thys/Relational_Forests/document/root.bib

thys/Relational_Forests/document/root.tex

web/entries/Aggregation_Algebras.html

web/entries/Bounded_Deducibility_Security.html

web/entries/Dirichlet_L.html

web/entries/Finitely_Generated_Abelian_Groups.html

web/entries/Fresh_Identifiers.html

web/entries/KAD.html

web/entries/MFMC_Countable.html

web/entries/Regex_Equivalence.html

web/entries/Relational_Disjoint_Set_Forests.html

web/entries/Relational_Forests.html

web/entries/Relational_Minimum_Spanning_Trees.html

web/entries/Relational_Paths.html

web/entries/SpecCheck.html

web/entries/Stone_Algebras.html

web/entries/Stone_Kleene_Relation_Algebras.html

web/entries/Stone_Relation_Algebras.html

web/entries/Subset_Boolean_Algebras.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html

merge from AFP 2021
7ca6a77befba
Actions