Diffusion afp-devel a8d1e146f641

merge from AFP 2019, broken: Priority_Search_Trees
a8d1e146f641
Actions

Tags

None

Subscribers

None

Description

merge from AFP 2019, broken: Priority_Search_Trees

Details

Provenance

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

Authored on

Parents

rAFPc625e8df309f: sitegen
rAFP676a75e041d9: more Order

Branches

Unknown

Tags

Unknown

Event Timeline

Merged Changes

676a75e041d9 more Order
Author
nipkow
Browse Repository
No Builds
No Audits
8a032c8c5b06 more Order
Author
nipkow
Browse Repository
No Builds
No Audits
683827a3f2a2 more Order
Author
nipkow
Browse Repository
No Builds
No Audits
26167902b4d2 more Order
Author
nipkow
Browse Repository
No Builds
No Audits
581aa08c667e abstracted from deterministic automata
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
86f544c41cb4 removed UNION
Author
nipkow
Browse Repository
No Builds
No Audits
d697df9a952b tuned
Author
nipkow
Browse Repository
No Builds
No Audits
3261ff4818d4 merge from afp-2019
Author
kleing
Browse Repository
No Builds
No Audits
ec3ff55171a9 tuned
Author
florian.haftmann
Browse Repository
No Builds
No Audits
967caff984be a few corollaries
Author
traytel
Browse Repository
No Builds
No Audits
023d4c3c8ef8 typo
Author
Christian Sternagel
Browse Repository
No Builds
No Audits
1099e41870d8 even more appropriate fact name
Author
florian.haftmann
Browse Repository
No Builds
No Audits
d91cf5dccf6a merged
Author
traytel
Browse Repository
No Builds
No Audits
76da667dfde4 tuned definition of value as suggested by an ITP reviewer
Author
traytel
Browse Repository
No Builds
No Audits
1c7ecec6a187 simplified proof
Author
nipkow
Browse Repository
No Builds
No Audits
c293c479d6b6 repaired proofs
Author
florian.haftmann
Browse Repository
No Builds
No Audits
a9d827f1c5b1 moved some theorems into HOL main corpus
Author
florian.haftmann
Browse Repository
No Builds
No Audits
65974f61a998 official fact collection sign_simps
Author
florian.haftmann
Browse Repository
No Builds
No Audits
415b7b57be74 dropped unused session references
Author
florian.haftmann
Browse Repository
No Builds
No Audits
0546343b94d3 clear separation of types for bits (False / True) and Z2 (0 / 1)
Author
florian.haftmann
Browse Repository
No Builds
No Audits
ee7d766eb01a dropped weaker legacy alias;
Author
florian.haftmann
Browse Repository
No Builds
No Audits
f6b91be1ab2d dropped former legacy input abbreviations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
cf0914a2304e fix for previous commit
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
6197fe173c6f refactoring
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
ad3aff5eb868 minor adjustments to automata library
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
60862c9ef07b refactored degeneralization
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
dc3e35215567 updated basic theories
Author
Julian Brunner <julianbrunner@gmail.com>
Browse Repository
No Builds
No Audits
22263520f4c8 updated with guillemot syntax
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
e6d3d109c89a updated to devel
Author
nipkow
Browse Repository
No Builds
No Audits
a5f6453144c6 fixed latex errors using babel
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
fb851cb1ca27 replaced ceiling brackets by guillemots
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
79d06abed2e0 consistency is provable
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
5c9417f37470 merge from afp-2019
Author
kleing
Browse Repository
No Builds
No Audits
a8e34b81e70f tuned timeout;
Author
makarius
Browse Repository
No Builds
No Audits
7149dd204040 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
87cfcf4d1dec update cartouches
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
ca143f3dbb79 LambdaAuth: remove lemmas moved to distribution
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
cd86f83a05bb merge from afp-2019
Author
kleing
Browse Repository
No Builds
No Audits
72f2f7d150d6 re-instate devel changeset 6edffc003761
Author
kleing
Browse Repository
No Builds
No Audits
753dc504efaf reset version to devel after release fork
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 (127)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

metadata/

Complete_Non_Orders

Binary_Relations.thy

Complete_Relations.thy

Fixed_Points.thy

Differential_Game_Logic

Coincidence.thy

Denotational_Semantics.thy

Differential_Game_Logic.thy

Identifiers.thy

Static_Semantics.thy

Abstract_Monitor.thy

Monitor_Code.thy

Prim_Dijkstra_Simple

Chapter_Dijkstra.thy

Chapter_Prim.thy

Dijkstra_Abstract.thy

Dijkstra_Impl.thy

Directed_Graph.thy

Directed_Graph_Impl.thy

Directed_Graph_Specs.thy

Prim_Abstract.thy

Undirected_Graph.thy

Undirected_Graph_Impl.thy

Undirected_Graph_Specs.thy

Priority_Search_Trees

PST_General.thy

Prio_Map_Specs.thy

Abs_Int_ITP2012.html

Abstract-Hoare-Logics.html

Algebraic_Numbers.html

Amortized_Complexity.html

ArrowImpossibilityGS.html

Berlekamp_Zassenhaus.html

Boolean_Expression_Checkers.html

CAVA_LTL_Modelchecker.html

Compiling-Exceptions-Correctly.html

Complete_Non_Orders.html

Containers.html

Density_Compiler.html

Differential_Game_Logic.html

Dynamic_Tables.html

Flyspeck-Tame.html

FunWithFunctions.html

FunWithTilings.html

Functional-Automata.html

Gauss-Jordan-Elim-Fun.html

Hoare_Time.html

HotelKeyCards.html

Jordan_Normal_Form.html

LLL_Basis_Reduction.html

LLL_Factorization.html

LinearQuantifierElim.html

List-Index.html

List_Update.html

MFOTL_Monitor.html

MSO_Regex_Equivalence.html

Markov_Models.html

Monad_Memo_DP.html

Native_Word.html

NormByEval.html

Optimal_BST.html

Pairing_Heap.html

Perron_Frobenius.html

Polynomial_Factorization.html

Polynomial_Interpolation.html

Prim_Dijkstra_Simple.html

Priority_Queue_Braun.html

Priority_Search_Trees.html

Propositional_Proof_Systems.html

Regex_Equivalence.html

Regular-Sets.html

Root_Balanced_Tree.html

Splay_Tree.html

Subresultants.html

Weight_Balanced_Trees.html

statistics.html

rAFPa8d1e146f641

metadata/metadata

thys/Complete_Non_Orders/Binary_Relations.thy

thys/Complete_Non_Orders/Complete_Relations.thy

thys/Complete_Non_Orders/Fixed_Points.thy

thys/Complete_Non_Orders/ROOT

thys/Complete_Non_Orders/document/root.bib

thys/Complete_Non_Orders/document/root.tex

thys/Differential_Game_Logic/Axioms.thy

thys/Differential_Game_Logic/Coincidence.thy

thys/Differential_Game_Logic/Denotational_Semantics.thy

thys/Differential_Game_Logic/Differential_Game_Logic.thy

thys/Differential_Game_Logic/Identifiers.thy

thys/Differential_Game_Logic/Ids.thy

thys/Differential_Game_Logic/Lib.thy

thys/Differential_Game_Logic/ROOT

thys/Differential_Game_Logic/Static_Semantics.thy

thys/Differential_Game_Logic/Syntax.thy

thys/Differential_Game_Logic/USubst.thy

thys/Differential_Game_Logic/document/root.bib

thys/Differential_Game_Logic/document/root.tex

thys/MFOTL_Monitor/Abstract_Monitor.thy

thys/MFOTL_Monitor/Examples.thy

thys/MFOTL_Monitor/Interval.thy

thys/MFOTL_Monitor/MFOTL.thy

thys/MFOTL_Monitor/Monitor.thy

thys/MFOTL_Monitor/Monitor_Code.thy

thys/MFOTL_Monitor/ROOT

thys/MFOTL_Monitor/Table.thy

thys/MFOTL_Monitor/Trace.thy

thys/MFOTL_Monitor/document/root.bib

thys/MFOTL_Monitor/document/root.tex

thys/Prim_Dijkstra_Simple/Chapter_Dijkstra.thy

thys/Prim_Dijkstra_Simple/Chapter_Prim.thy

thys/Prim_Dijkstra_Simple/Common.thy

thys/Prim_Dijkstra_Simple/Dijkstra_Abstract.thy

thys/Prim_Dijkstra_Simple/Dijkstra_Impl.thy

thys/Prim_Dijkstra_Simple/Directed_Graph.thy

thys/Prim_Dijkstra_Simple/Directed_Graph_Impl.thy

thys/Prim_Dijkstra_Simple/Directed_Graph_Specs.thy

thys/Prim_Dijkstra_Simple/Prim_Abstract.thy

thys/Prim_Dijkstra_Simple/Prim_Impl.thy

thys/Prim_Dijkstra_Simple/ROOT

thys/Prim_Dijkstra_Simple/Undirected_Graph.thy

thys/Prim_Dijkstra_Simple/Undirected_Graph_Impl.thy

thys/Prim_Dijkstra_Simple/Undirected_Graph_Specs.thy

thys/Prim_Dijkstra_Simple/document/root.bib

thys/Prim_Dijkstra_Simple/document/root.tex

thys/Priority_Search_Trees/PST_General.thy

thys/Priority_Search_Trees/PST_RBT.thy

thys/Priority_Search_Trees/Prio_Map_Specs.thy

thys/Priority_Search_Trees/ROOT

thys/Priority_Search_Trees/document/root.bib

thys/Priority_Search_Trees/document/root.tex

thys/ROOTS

web/entries/AVL-Trees.html

web/entries/Abs_Int_ITP2012.html

web/entries/Abstract-Hoare-Logics.html

web/entries/Algebraic_Numbers.html

web/entries/Amortized_Complexity.html

web/entries/ArrowImpossibilityGS.html

web/entries/Berlekamp_Zassenhaus.html

web/entries/Boolean_Expression_Checkers.html

web/entries/CAVA_LTL_Modelchecker.html

web/entries/Compiling-Exceptions-Correctly.html

web/entries/Complete_Non_Orders.html

web/entries/Containers.html

web/entries/Density_Compiler.html

web/entries/Deriving.html

web/entries/Differential_Game_Logic.html

web/entries/Dynamic_Tables.html

web/entries/Flyspeck-Tame.html

web/entries/FunWithFunctions.html

web/entries/FunWithTilings.html

web/entries/Functional-Automata.html

web/entries/Gauss-Jordan-Elim-Fun.html

web/entries/Hoare_Time.html

web/entries/HotelKeyCards.html

web/entries/Jinja.html

web/entries/Jordan_Normal_Form.html

web/entries/LLL_Basis_Reduction.html

web/entries/LLL_Factorization.html

web/entries/LinearQuantifierElim.html

web/entries/List-Index.html

web/entries/List_Update.html

web/entries/MFOTL_Monitor.html

web/entries/MSO_Regex_Equivalence.html

web/entries/Markov_Models.html

web/entries/Marriage.html

web/entries/MiniML.html

web/entries/Monad_Memo_DP.html

web/entries/Native_Word.html

web/entries/NormByEval.html

web/entries/Optimal_BST.html

web/entries/Pairing_Heap.html

web/entries/Perron_Frobenius.html

web/entries/Polynomial_Factorization.html

web/entries/Polynomial_Interpolation.html

web/entries/Prim_Dijkstra_Simple.html

web/entries/Priority_Queue_Braun.html

web/entries/Priority_Search_Trees.html

web/entries/Propositional_Proof_Systems.html

web/entries/Regex_Equivalence.html

web/entries/Regular-Sets.html

web/entries/Root_Balanced_Tree.html

web/entries/Skew_Heap.html

web/entries/Splay_Tree.html

web/entries/Subresultants.html

web/entries/Treaps.html

web/entries/Trie.html

web/entries/Weight_Balanced_Trees.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html