afp-devel
6d89d20f7c88
Actions

Description

Automated merge with https://foss.heptapod.net/isa-afp/afp-devel

Details

Provenance

Andreas Lochbihler <mail@andreas-lochbihler.de>

Authored on

Parents

rAFP93ca33f4d915: a simpler MFMC proof for bounded networks
rAFPcb82935ea66a: Added ubx optimization of store instructions

Branches

Unknown

Tags

Unknown

Event Timeline

Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP6d89d20f7c88: Automated merge with https://foss.heptapod.net/isa-afp/afp-devel.Dec 19 2020, 10:47 AM

Merged Changes

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

cb82935ea66a Added ubx optimization of store instructions
Author
desharna
Browse Repository
No Builds
No Audits
6c81363206e4 Remove redundant session qualifiers on a few imports, which seem to confuse…
Author
"Eugene W. Stark <stark@cs.stonybrook.edu>"
Browse Repository
No Builds
No Audits
54c305a39abc Fixed proofs indicated by Isabelle/Jenkins
Author
Jonathan Julian Huerta y Munive <jonjulian23@gmail.com>
Browse Repository
No Builds
No Audits
a9a967ae13a7 Added components based on Kleene algebras with tests. These implement…
Author
Jonathan Julian Huerta y Munive <jonjulian23@gmail.com>
Browse Repository
No Builds
No Audits
1cc03815b90c replaced concrete nat and bool by abstract types
Author
desharna
Browse Repository
No Builds
No Audits
b8e228d01fed adapted to Isabelle/fd8d82c4433b;
Author
makarius
Browse Repository
No Builds
No Audits
2b91ed6879db Relational_Disjoint_Set_Forests, Stone_Relation_Algebras…
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
0c20abab24ee adapted to devel
Author
nipkow
Browse Repository
No Builds
No Audits
dbb9bfaf4283 Aggregation_Algebras: removed Hoare logic (now in HOL-Hoare) and spanning trees…
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
eecfc3c9b79e Aggregation_Algebras: removed Hoare logic (now in HOL-Hoare) and spanning trees…
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
4010aa481e6c Relational_Disjoint_Set_Forests, Relational_Minimum_Spanning_Trees: minor edit…
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
31421e50c01b Relational_Minimum_Spanning_Trees: minor changes to make it work with…
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
8442fc1cb727 Relational_Method: adjustments for isabelle f0fa51227a23
Author
kleing
Browse Repository
No Builds
No Audits
c0f91ac420e7 merge from afp-2020
Author
kleing
Browse Repository
No Builds
No Audits
cd33914660a2 regenerate website with new bibtex
Author
kleing
Browse Repository
No Builds
No Audits
8234453a0f91 Use HTTPS in BibTeX URLs (by Martin Desharnais)
Author
kleing
Browse Repository
No Builds
No Audits
058bb35d2e69 adjust Isabelle_Marries_Dirac to isabelle f0fa51227a23
Author
kleing
Browse Repository
No Builds
No Audits
91ca4136b53f merge from afp-2020
Author
kleing
Browse Repository
No Builds
No Audits
bea58471d96a Updated version by author
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
1dedec1ce4fc New entry: Relational_Minimum_Spanning_Trees
Author
nipkow
Browse Repository
No Builds
No Audits
caaedd506d3d Relational_Method website
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
cdc40199823d new entry Relational_Method
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
b33e4e32b4ec merge
Author
kleing
Browse Repository
No Builds
No Audits
5728774bf660 fix sitegen warning
Author
kleing
Browse Repository
No Builds
No Audits
c739e71fd6ff new entry Finite-Map-Extras
Author
kleing
Browse Repository
No Builds
No Audits
ab7cbd1a97a5 sitegen, new topics for quantum compution/information
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
65d5538f1b4b new entry Isabelle marries Dirac
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
01a2d304855c New entry Interpreter_Optimizations
Author
nipkow
Browse Repository
No Builds
No Audits
77790ea69409 avoid generated code in versioning -- ONLY PARTIALLY TESTED DUE TO NON-SELF…
Author
florian.haftmann
Browse Repository
No Builds
No Audits
af0298e0b819 moved some lemmas from AFP to distribution
Author
florian.haftmann
Browse Repository
No Builds
No Audits
59470eb9f5ab sorted out lemmas
Author
florian.haftmann
Browse Repository
No Builds
No Audits
64ea6f2d9e8c Relational_Paths: minor edit, now uses HOL-Hoare
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
1998678fe699 adapted to devel
Author
nipkow
Browse Repository
No Builds
No Audits
074cac8ca43a Saturation Framework: minor fixes
Author
Sophie Tourret <stourret@mpi-inf.mpg.de>
Browse Repository
No Builds
No Audits
bcbda9a982dc more generous timeout;
Author
makarius
Browse Repository
No Builds
No Audits
5d155a850a33 more generous timeout;
Author
makarius
Browse Repository
No Builds
No Audits
47cff1c3c5c9 redundant;
Author
makarius
Browse Repository
No Builds
No Audits
f59bb635da5b more generous timeout;
Author
makarius
Browse Repository
No Builds
No Audits
391fd487234d renamed confusingly named predicate
Author
blanchette
Browse Repository
No Builds
No Audits
e06e6a6a8ac4 tuned whitespace;
Author
makarius
Browse Repository
No Builds
No Audits
009fa5ffc3e6 sorted out lemmas
Author
florian.haftmann
Browse Repository
No Builds
No Audits
921126ac4dd1 adapted to Isabelle/5f9d66155081;
Author
makarius
Browse Repository
No Builds
No Audits
98774839d1ee Update change history. Fix a typo.
Author
"Eugene W. Stark <stark@cs.stonybrook.edu>"
Browse Repository
No Builds
No Audits
1c6c1d15536e adjusting for the re-orientation of order_unique_lemma
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
a13bec92d3d2 opening is now a keyword
Author
florian.haftmann
Browse Repository
No Builds
No Audits
69f3a2dbc505 sorted out lemmas
Author
florian.haftmann
Browse Repository
No Builds
No Audits
11e9abcf7366 2 new devel entries: DOM_Components and Shadow_DOM
Author
kleing
Browse Repository
No Builds
No Audits
707413df05fd merge from afp-2020
Author
kleing
Browse Repository
No Builds
No Audits
cace3e947231 SC_DOM_Components website
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
93ce0b890f00 entry SC_DOM_Components
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits

Changes (13)

Path

Size

thys

MFMC_Countable

MFMC_Bounded.thy

MFMC_Flow_Attainability.thy

Matrix_For_Marginals.thy

Max_Flow_Min_Cut_Countable.thy

ROOT

document/

root.bib

rAFP6d89d20f7c88

View Options

thys/MFMC_Countable/MFMC_Bounded.thy

View Options

thys/MFMC_Countable/MFMC_Flow_Attainability.thy

View Options

thys/MFMC_Countable/MFMC_Misc.thy

View Options

thys/MFMC_Countable/MFMC_Network.thy

View Options

thys/MFMC_Countable/MFMC_Reduction.thy

View Options

thys/MFMC_Countable/MFMC_Unbounded.thy

View Options

thys/MFMC_Countable/MFMC_Web.thy

View Options

thys/MFMC_Countable/Matrix_For_Marginals.thy

View Options

thys/MFMC_Countable/Max_Flow_Min_Cut_Countable.thy

View Options

thys/MFMC_Countable/ROOT

View Options

thys/MFMC_Countable/document/root.bib

Automated merge with https://foss.heptapod.net/isa-afp/afp-devel6d89d20f7c88Actions

Description

Details

Event Timeline

Merged Changes

Changes (13)

rAFP6d89d20f7c88

thys/MFMC_Countable/MFMC_Bounded.thy

thys/MFMC_Countable/MFMC_Flow_Attainability.thy

thys/MFMC_Countable/MFMC_Misc.thy

thys/MFMC_Countable/MFMC_Network.thy

thys/MFMC_Countable/MFMC_Reduction.thy

thys/MFMC_Countable/MFMC_Unbounded.thy

thys/MFMC_Countable/MFMC_Web.thy

thys/MFMC_Countable/Matrix_For_Marginals.thy

thys/MFMC_Countable/Max_Flow_Min_Cut_Countable.thy

thys/MFMC_Countable/ROOT

thys/MFMC_Countable/document/root.bib

Automated merge with https://foss.heptapod.net/isa-afp/afp-devel
6d89d20f7c88
Actions