Diffusion afp-devel c5e379424280

Merge updates on dynamic programming
c5e379424280
Actions

Description

Merge updates on dynamic programming

Details

Provenance

Simon Wimmer <wimmers@in.tum.de>

Authored on

Parents

rAFP78ceb5a9dbb1: Cleaned
rAFPfabc5f83d7ed: merged

Branches

Unknown

Tags

Unknown

Event Timeline

Simon Wimmer <wimmers@in.tum.de> committed rAFPc5e379424280: Merge updates on dynamic programming.Jan 18 2021, 3:37 PM

Merged Changes

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

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
bfb55826ffc0 New entry Hood_Melville_Queue
Author
nipkow
Browse Repository
No Builds
No Audits
7f80012e5998 Adapted to 2021-RC2; renamed lemma ccc_Fn_nat -> ccc_Fn_2
Author
sterraf
Browse Repository
No Builds
No Audits
fabc5f83d7ed merged
Author
nipkow
Browse Repository
No Builds
No Audits
84c055f7b95d more explicit proof
Author
nipkow
Browse Repository
No Builds
No Audits
21348d1ad4c9 sync Word_Lib with l4v
Author
kleing
Browse Repository
No Builds
No Audits
4ee343798f76 adapted to scala-2.13.4;
Author
makarius
Browse Repository
No Builds
No Audits
c7606b58bd03 removed a terrible default simprule
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
601908994b57 Word_Lib: spelling
Author
kleing
Browse Repository
No Builds
No Audits
52bcf666e8c7 CSP_RefTK: adjust for Isabelle 1105c42722dc
Author
kleing
Browse Repository
No Builds
No Audits
f7ada09942ba merge from afp-2020
Author
kleing
Browse Repository
No Builds
No Audits
dd8e0cdca49e sitegen for CSP_RefTK
Author
pruvisto
Browse Repository
No Builds
No Audits
626c957d2647 New submission: CSP_RefTK
Author
pruvisto
Browse Repository
No Builds
No Audits
2da14e4d854f webpage for Delta_System_Lemma
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
89ed1831f6cd New (ZF!) entry Delta_System_Lemma
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
a80f4e41ac2b sitegen and metadata
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
85bc7487435c new entry: Topological_Semantics
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
03248eeafe63 Algebraic_Numbers: some material on algebraic integers
Author
pruvisto
Browse Repository
No Builds
No Audits
37f216da1cab merged
Author
makarius
Browse Repository
No Builds
No Audits
77d6721f525d tuned -- avoid old-style verbatim text;
Author
makarius
Browse Repository
No Builds
No Audits
0d86fcd673f9 isabelle update_cartouches;
Author
makarius
Browse Repository
No Builds
No Audits
7e9db34de4f6 A bit of tidying
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
877ead9ac185 merge
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
29cb2568407d reform
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
55b144f95853 added code-post lemma for algebraic numbers
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
7661a1e15035 moved lemmas such that algebraic numbers theory is not importing factorization…
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
95ca3e871eb7 moved lemmas
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
306f9dbda4f6 proper indentation
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
1a49a0b2203e cleanup
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
c1ae04538bfe merged
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
d3642bed65b1 fix long-running proof
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
5d1dd3139576 updated benchmark scripts for iFM paper
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
f972abc8ec2e Update ConcurrentGC
Author
Peter Gammie <peteg42@gmail.com>
Browse Repository
No Builds
No Audits
5ee9691b6e09 Update ConcurrentIMP
Author
Peter Gammie <peteg42@gmail.com>
Browse Repository
No Builds
No Audits
8bf81decb8ac adapted to isabelle-dev/74be162a47cd: added some renamings that were missed…
Author
pruvisto
Browse Repository
No Builds
No Audits
dfe83cc412a3 adapted to isabelle-dev/74be162a47cd
Author
pruvisto
Browse Repository
No Builds
No Audits
a31f698ef3f8 avoid multiple uses of the same ML file;
Author
makarius
Browse Repository
No Builds
No Audits
0668d43edb22 more standard ML file/module names;
Author
makarius
Browse Repository
No Builds
No Audits
824acfe540c7 more standard headers;
Author
makarius
Browse Repository
No Builds
No Audits
459344fb0c40 Isabelle_Meta_Model: avoid multiple use of ML_file
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
0327fb7d3352 ensure that at least an empty report file exists
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
0c0f25783758 delete report file if already exists
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
7b26d4cc3c17 A few tweaks
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits

Changes (4)

Path

Size

thys/

Monad_Memo_DP/

example/

rAFPc5e379424280

View Options

thys/Monad_Memo_DP/example/Bellman_Ford.thy

View Options

thys/Monad_Memo_DP/example/CYK.thy

View Options

thys/Monad_Memo_DP/example/Min_Ed_Dist0.thy

View Options

thys/Monad_Memo_DP/example/OptBST.thy

Merge updates on dynamic programmingc5e379424280Actions

Description

Details

Event Timeline

Merged Changes

Changes (4)

rAFPc5e379424280

thys/Monad_Memo_DP/example/Bellman_Ford.thy

thys/Monad_Memo_DP/example/CYK.thy

thys/Monad_Memo_DP/example/Min_Ed_Dist0.thy

thys/Monad_Memo_DP/example/OptBST.thy

Merge updates on dynamic programming
c5e379424280
Actions