Diffusion afp-devel e10739c4e48f

merge from AFP 2019
e10739c4e48f
Actions

Tags

None

Subscribers

None

Description

merge from AFP 2019

Details

Provenance

Rene Thiemann <rene.thiemann@uibk.ac.at>

Authored on

Parents

rAFP600b62ce0cc9: minor adjustment of internal interface of simplex (fun -> mapping),
rAFPe30fe5fba4d7: Merged

Branches

Unknown

Tags

Unknown

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPe10739c4e48f: merge from AFP 2019.Dec 2 2019, 12:58 PM

Merged Changes

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

e30fe5fba4d7 Merged
Author
pruvisto
Browse Repository
No Builds
No Audits
4f482d20a008 adapted to isabelle-dev 954ee5acaae0
Author
pruvisto
Browse Repository
No Builds
No Audits
e8bc925a7952 adapted to Isabelle/0c47c128f9af;
Author
Wenda Li <liwenda1990@hotmail.com>
Browse Repository
No Builds
No Audits
7e45833c40f6 explicit variable declaration
Author
florian.haftmann
Browse Repository
No Builds
No Audits
78025c98b739 adapted to Isabelle/592e2afdd50c;
Author
makarius
Browse Repository
No Builds
No Audits
6128683958ca more realistic timeout;
Author
makarius
Browse Repository
No Builds
No Audits
c47ca19eaae3 proper prefix syntax
Author
florian.haftmann
Browse Repository
No Builds
No Audits
7e7b23d02d4b removed unused auxiliary lemmas
Author
florian.haftmann
Browse Repository
No Builds
No Audits
87c3943758c0 More about Bernoulli numbers
Author
pruvisto
Browse Repository
No Builds
No Audits
5580004cc074 Added von Staudt–Clausen theorem to Bernoulli
Author
pruvisto
Browse Repository
No Builds
No Audits
f1ef07c47429 don't build Linear_Programming on Mac
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
54f6a4f1d8a3 updated to fdb6c5034c24
Author
nipkow
Browse Repository
No Builds
No Audits
2a06a089800f merged
Author
immler
Browse Repository
No Builds
No Audits
c5944c920143 moved Interval and Interval_Approximation to isabelle
Author
immler
Browse Repository
No Builds
No Audits
3f2bdb753c38 patched a proof
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c5c88012f116 fixed a failing (and ugly) proof
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
1f17a5f5a1e2 Merge branch
Author
Andreas Halkjær From <s144442@student.dtu.dk>
Browse Repository
No Builds
No Audits
f05300d8017a Tuned spacing.
Author
Andreas Halkjær From <s144442@student.dtu.dk>
Browse Repository
No Builds
No Audits
877fab13602e follow devel changeset 581083959358
Author
nipkow
Browse Repository
No Builds
No Audits
1a0be182fdda Consistent spacing in set comprehension and name fixes.
Author
Andreas Halkjær From <s144442@student.dtu.dk>
Browse Repository
No Builds
No Audits
616e41c5089c Consistent spacing in set comprehension.
Author
Andreas Halkjær From <s144442@student.dtu.dk>
Browse Repository
No Builds
No Audits
ba01b2eda5e4 updated email
Author
nipkow
Browse Repository
No Builds
No Audits
c85fcabd5bff avoid name clash of internal derivations;
Author
makarius
Browse Repository
No Builds
No Audits
9bd3fa01955a recovered proof;
Author
makarius
Browse Repository
No Builds
No Audits
6a3c69467146 Clean: ROOT/directories structure
Author
kleing
Browse Repository
No Builds
No Audits
2ac9ae9dd0f6 Clean: consolidate ROOT file for new session directories
Author
kleing
Browse Repository
No Builds
No Audits
48295c330a18 merge from afp-2019
Author
kleing
Browse Repository
No Builds
No Audits
c7faf745010f moved quickcheck setup to distribution
Author
florian.haftmann
Browse Repository
No Builds
No Audits
c30a1164293a moved generic instance to distribution
Author
florian.haftmann
Browse Repository
No Builds
No Audits
02b9d0561118 recovered proofs;
Author
makarius
Browse Repository
No Builds
No Audits
e92e80d9cb16 made NBA translation explicit
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
f9adabfbcca6 merge
Author
Giuliano Losa <giuliano@losa.fr>
Browse Repository
No Builds
No Audits
dd760b1d41e5 add a section about Stellar's intact sets
Author
Giuliano Losa <giuliano@losa.fr>
Browse Repository
No Builds
No Audits
2382848477ea Add lemma strong_cluster_union
Author
Giuliano Losa <giuliano@losa.fr>
Browse Repository
No Builds
No Audits
93099fba4c66 Remove spurious W variable in locale assumption
Author
Giuliano Losa <giuliano@losa.fr>
Browse Repository
No Builds
No Audits
381f2aa05ed3 avoid sign_simps in favour of algebra_split_simps
Author
florian.haftmann
Browse Repository
No Builds
No Audits
12ac7c824ad0 Moved some lemmas about limits to Complex_Main
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
d7a872772538 formally augmented corresponding rules for field_simps
Author
florian.haftmann
Browse Repository
No Builds
No Audits
ab79744bf7a0 updated to work with recent automata changes
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
83c109099c9b added NGBA implementations
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
a0ad86208e23 adjusted NBA implementation
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
a7cac9b35489 added NBA combination nodes theorems, minor adjustments
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
dfe6b2a998fe refer to explicit ISABELLE_DOT instead of implicit PATH;
Author
makarius
Browse Repository
No Builds
No Audits
dfa7db541b8e avoid name clash of internal derivations;
Author
makarius
Browse Repository
No Builds
No Audits
1f139e059475 avoid name clash of internal derivations;
Author
makarius
Browse Repository
No Builds
No Audits
29b3e29e042e proper Consts.dummy_types;
Author
makarius
Browse Repository
No Builds
No Audits
dcb063b90519 updated to devel
Author
nipkow
Browse Repository
No Builds
No Audits
66bfe59e1850 Moving a bit more material into the Analysis library
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c3a70e5ad56b Removal of material now in Isabelle's libraries
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
ee2ef0deb899 updated to devel
Author
nipkow
Browse Repository
No Builds
No Audits

Changes (107)

Path

Size

metadata/

templates/

Interval_Arithmetic_Word32

Finite_String.thy

Interpreter.thy

Interval_Word32.thy

Simplex/

Simplex_Incremental.thy

Challenge1A.thy

Challenge1B.thy

Challenge2A.thy

Challenge2B.thy

Parallel_Multiset_Fold.thy

Exc_Nres_Monad.thy

ZFC_Cardinals.thy

ZFC_Library.thy

ZFC_Typeclasses.thy

Abstract-Rewriting.html

Algebraic_Numbers.html

Automatic_Refinement.html

Berlekamp_Zassenhaus.html

Binomial-Heaps.html

Bounded_Deducibility_Security.html

CAVA_Automata.html

CAVA_LTL_Modelchecker.html

Collections.html

Containers.html

DFS_Framework.html

Datatype_Order_Generator.html

Dijkstra_Shortest_Path.html

EdmondsKarp_Maxflow.html

Efficient-Mergesort.html

Finger-Trees.html

Flow_Networks.html

Floyd_Warshall.html

Formula_Derivatives.html

Gauss_Jordan.html

Hidden_Markov_Models.html

Interval_Arithmetic_Word32.html

Knuth_Morris_Pratt.html

LTL_Master_Theorem.html

LTL_to_GBA.html

Linear_Recurrences.html

Monad_Memo_DP.html

Native_Word.html

Ordinary_Differential_Equations.html

Partial_Order_Reduction.html

Polynomial_Factorization.html

Polynomial_Interpolation.html

Pratt_Certificate.html

Prim_Dijkstra_Simple.html

Priority_Search_Trees.html

Probabilistic_Timed_Automata.html

Probabilistic_While.html

Program-Conflict-Analysis.html

Prpu_Maxflow.html

Refine_Imperative_HOL.html

Refine_Monadic.html

Separation_Logic_Imperative_HOL.html

Subresultants.html

Timed_Automata.html

Tree-Automata.html

VectorSpace.html

VerifyThis2018.html

VerifyThis2019.html

ZFC_in_HOL.html

statistics.html

rAFPe10739c4e48f

metadata/metadata

Loading...

metadata/templates/download.tpl

Loading...

metadata/topics

Loading...

thys/Interval_Arithmetic_Word32/Finite_String.thy

Loading...

thys/Interval_Arithmetic_Word32/Interpreter.thy

Loading...

thys/Interval_Arithmetic_Word32/Interval_Word32.thy

Loading...

thys/Interval_Arithmetic_Word32/ROOT

Loading...

thys/Interval_Arithmetic_Word32/document/root.bib

Loading...

thys/Interval_Arithmetic_Word32/document/root.tex

Loading...

thys/ROOTS

Loading...

thys/Simplex/Simplex_Incremental.thy

Loading...

thys/VerifyThis2019/Challenge1A.thy

Loading...

thys/VerifyThis2019/Challenge1B.thy

Loading...

thys/VerifyThis2019/Challenge2A.thy

Loading...

thys/VerifyThis2019/Challenge2B.thy

Loading...

thys/VerifyThis2019/Challenge3.thy

Loading...

thys/VerifyThis2019/Parallel_Multiset_Fold.thy

Loading...

thys/VerifyThis2019/ROOT

Loading...

thys/VerifyThis2019/document/root.tex

Loading...

thys/VerifyThis2019/lib/Exc_Nres_Monad.thy

Loading...

thys/VerifyThis2019/lib/VTcomp.thy

Loading...

thys/ZFC_in_HOL/Kirby.thy

Loading...

thys/ZFC_in_HOL/ROOT

Loading...

thys/ZFC_in_HOL/ZFC_Cardinals.thy

Loading...

thys/ZFC_in_HOL/ZFC_Library.thy

Loading...

thys/ZFC_in_HOL/ZFC_Typeclasses.thy

Loading...

thys/ZFC_in_HOL/ZFC_in_HOL.thy

Loading...

thys/ZFC_in_HOL/document/root.bib

Loading...

thys/ZFC_in_HOL/document/root.tex

Loading...

web/download.html

Loading...

web/entries/Abstract-Rewriting.html

Loading...

web/entries/Algebraic_Numbers.html

Loading...

web/entries/Automatic_Refinement.html

Loading...

web/entries/Berlekamp_Zassenhaus.html

Loading...

web/entries/Binomial-Heaps.html

Loading...

web/entries/Bounded_Deducibility_Security.html

Loading...

web/entries/CAVA_Automata.html

Loading...

web/entries/CAVA_LTL_Modelchecker.html

Loading...

web/entries/Collections.html

Loading...

web/entries/Containers.html

Loading...

web/entries/DFS_Framework.html

Loading...

web/entries/Datatype_Order_Generator.html

Loading...

web/entries/Deriving.html

Loading...

web/entries/Dijkstra_Shortest_Path.html

Loading...

web/entries/EdmondsKarp_Maxflow.html

Loading...

web/entries/Efficient-Mergesort.html

Loading...

web/entries/Finger-Trees.html

Loading...

web/entries/Flow_Networks.html

Loading...

web/entries/Floyd_Warshall.html

Loading...

web/entries/Formula_Derivatives.html

Loading...

web/entries/Gabow_SCC.html

Loading...

web/entries/Gauss_Jordan.html

Loading...

web/entries/Hidden_Markov_Models.html

Loading...

web/entries/HyperCTL.html

Loading...

web/entries/IMP2.html

Loading...

web/entries/Interval_Arithmetic_Word32.html

Loading...

web/entries/Knuth_Morris_Pratt.html

Loading...

web/entries/Kruskal.html

Loading...

web/entries/LTL_Master_Theorem.html

Loading...

web/entries/LTL_to_GBA.html

Loading...

web/entries/Lehmer.html

Loading...

web/entries/Linear_Recurrences.html

Loading...

web/entries/Matrix.html

Loading...

web/entries/Monad_Memo_DP.html

Loading...

web/entries/Native_Word.html

Loading...

web/entries/Optics.html

Loading...

web/entries/Ordinary_Differential_Equations.html

Loading...

web/entries/Partial_Order_Reduction.html

Loading...

web/entries/Polynomial_Factorization.html

Loading...

web/entries/Polynomial_Interpolation.html

Loading...

web/entries/Pratt_Certificate.html

Loading...

web/entries/Prim_Dijkstra_Simple.html

Loading...

web/entries/Priority_Search_Trees.html

Loading...

web/entries/Probabilistic_Timed_Automata.html

Loading...

web/entries/Probabilistic_While.html

Loading...

web/entries/Program-Conflict-Analysis.html

Loading...

web/entries/Promela.html

Loading...

web/entries/Prpu_Maxflow.html

Loading...

web/entries/ROBDD.html

Loading...

web/entries/Refine_Imperative_HOL.html

Loading...

web/entries/Refine_Monadic.html

Loading...

web/entries/Separation_Logic_Imperative_HOL.html

Loading...

web/entries/Show.html

Loading...

web/entries/Subresultants.html

Loading...

web/entries/Timed_Automata.html

Loading...

web/entries/Tree-Automata.html

Loading...

web/entries/Trie.html

Loading...

web/entries/UTP.html

Loading...

web/entries/VectorSpace.html

Loading...

web/entries/VerifyThis2018.html

Loading...

web/entries/VerifyThis2019.html

Loading...

web/entries/Word_Lib.html

Loading...

web/entries/ZFC_in_HOL.html

Loading...

web/index.html

Loading...

web/rss.xml

Loading...

web/statistics.html

Loading...

web/topics.html

Loading...