Diffusion afp-devel e69090abc053

Merged
e69090abc053
Actions

Description

Merged

Details

Provenance

Simon Wimmer <wimmers@in.tum.de>

Authored on

Parents

rAFPc5e379424280: Merge updates on dynamic programming
rAFPbfb55826ffc0: New entry Hood_Melville_Queue

Branches

Unknown

Tags

Unknown

Event Timeline

Simon Wimmer <wimmers@in.tum.de> committed rAFPe69090abc053: Merged.Jan 18 2021, 10:44 PM

Merged Changes

c5e379424280 Merge updates on dynamic programming
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
78ceb5a9dbb1 Cleaned
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
0eac2d7a263d Added example and tuned proof
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
1190a08539dc Make slice abbreviation input only
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
cddd9b09f0d0 Added bellman-ford implementation with detection of negative cycles
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
278bc88810fe Only one definition of path and weight functions
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
daebb0e27b64 Tuned proof automation
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
b9ca92c46cd9 Cleaning
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
1171b510ad2a Finished main theorems on Bellman-Ford
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
3944d6a35a00 Progress on true shortest paths
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
bd778b1f0c60 Cleaning
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
d0819b6e17c9 Closed sorries
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
6c027266d53e Fixed guess
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
67e783e1f268 Fixed sorries
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
b9514d50aa5a Simplified proof
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
1c40d029c4bd Cycle detection lemma
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
e3b9d924eefa Improved proof of main correctness theorem for BF
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
471f6ebae9a4 Scott continuity not assuming strictness
Author
Akihisa Yamada <akihisa.yamada@aist.go.jp>
Browse Repository
No Builds
No Audits
7812e4b5109f updated description
Author
Akihisa Yamada <akihisa.yamada@aist.go.jp>
Browse Repository
No Builds
No Audits
a744362b6529 forgotten commits
Author
Akihisa Yamada <akihisa.yamada@aist.go.jp>
Browse Repository
No Builds
No Audits
01c79f4098cd updating entry for LMCS submission
Author
Akihisa Yamada <akihisa.yamada@aist.go.jp>
Browse Repository
No Builds
No Audits
4ae553526864 Merge
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
016604dd1cab tidied a definition and proof
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c27ff156ee88 fix(scala): Updated code for 2.13
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
b4690943adb9 Updated comment
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
3b5ff4b8d37d Closing branch "devel"
Author
kleing
Browse Repository
No Builds
No Audits
a0d561998f20 closed branch
Author
kleing
Browse Repository
No Builds
No Audits
8e995d947fb0 closed pull-request branch
Author
Gerwin Klein <gerwin.klein@nicta.com.au>
Browse Repository
No Builds
No Audits
249c2b58d173 closed merged branch
Author
Gerwin Klein <gerwin.klein@nicta.com.au>
Browse Repository
No Builds
No Audits
ad14484777fc merged
Author
gerwin.klein@nicta.com.au
Browse Repository
No Builds
No Audits
e3e858bfc9eb merged
Author
kleing
Browse Repository
No Builds
No Audits
4bea345493dd Closed branch ltl
Author
Salomon Sickert <sickert@in.tum.de>
Browse Repository
No Builds
No Audits
53421953ad96 WIP/LTL Entry
Author
Salomon Sickert <sickert@in.tum.de>
Browse Repository
No Builds
No Audits

Changes (19)

Path

Size

metadata/

Delta_System_Lemma/

Hood_Melville_Queue.thy

Hood_Melville_Queue.html

rAFPe69090abc053

View Options

metadata/metadata

View Options

thys/Delta_System_Lemma/Cardinal_Library.thy

View Options

thys/Delta_System_Lemma/Cohen_Posets.thy

View Options

thys/Delta_System_Lemma/Konig.thy

View Options

thys/Hood_Melville_Queue/Hood_Melville_Queue.thy

View Options

thys/Hood_Melville_Queue/ROOT

View Options

thys/Hood_Melville_Queue/document/root.bib

View Options

thys/Hood_Melville_Queue/document/root.tex

View Options

thys/ROOTS

View Options

web/entries/Hood_Melville_Queue.html

View Options

web/index.html

View Options

web/rss.xml

View Options

web/statistics.html

View Options

Mergede69090abc053Actions

Description

Details

Event Timeline

Merged Changes

Changes (19)

rAFPe69090abc053

metadata/metadata

thys/Delta_System_Lemma/Cardinal_Library.thy

thys/Delta_System_Lemma/Cohen_Posets.thy

thys/Delta_System_Lemma/Konig.thy

thys/Hood_Melville_Queue/Hood_Melville_Queue.thy

thys/Hood_Melville_Queue/ROOT

thys/Hood_Melville_Queue/document/root.bib

thys/Hood_Melville_Queue/document/root.tex

thys/ROOTS

web/entries/Hood_Melville_Queue.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html

Merged
e69090abc053
Actions