Diffusion afp-devel 17e46e9fdfda

merge from afp-2021
17e46e9fdfda
Actions

Tags

None

Subscribers

None

Description

merge from afp-2021

Details

Provenance

Authored on

Parents

rAFP0c83e74a221f: simplify usage instructions more
rAFP5b451178b788: merged

Branches

Unknown

Tags

Unknown

Event Timeline

kleing committed rAFP17e46e9fdfda: merge from afp-2021.May 24 2021, 2:23 AM

Merged Changes

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

5b451178b788 merged
Author
makarius
Browse Repository
No Builds
No Audits
2c2eaa6a32e2 adapted to Isabelle/ef1a18e20ace;
Author
makarius
Browse Repository
No Builds
No Audits
5b4eeafc4c58 recover some patches after years of continuously changing Isabelle LaTeX output;
Author
makarius
Browse Repository
No Builds
No Audits
83bb072c2a8b prefer document_preprocessor over document_build;
Author
makarius
Browse Repository
No Builds
No Audits
7277415751d4 prefer document_logo instead of document_build script;
Author
makarius
Browse Repository
No Builds
No Audits
b08597803da3 proper options;
Author
makarius
Browse Repository
No Builds
No Audits
e28d0bec47d2 PATCH to Auto2 (for sorted) by Bohua, pending a permanent generalisation of…
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
fc32ad9925ee fixed two more "sorted" errors
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
fdbe2f5933e8 fixed two "sorted" issues
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
cb0adfb311e1 merged
Author
paulson
Browse Repository
No Builds
No Audits
02b3a52be010 changes for "sorted" as an abbreviation
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
e766628a0795 mere abbreviation for logical alias
Author
florian.haftmann
Browse Repository
No Builds
No Audits
75faf142b4be eliminated odd clone (see Isabelle/caa5a257d3ed);
Author
makarius
Browse Repository
No Builds
No Audits
e93051f65b1a strict_sorted now an abbreviation
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
41cc428000e3 merged
Author
paulson
Browse Repository
No Builds
No Audits
a757f7e7c954 deleted needless material
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
a19043a5f828 explicit type class operations for type-specific implementations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
a055a33fcb58 next step to phase out ancient numerals
Author
florian.haftmann
Browse Repository
No Builds
No Audits
8ff1ebba38da more small simplifications
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
26d8da1ea081 merged
Author
paulson
Browse Repository
No Builds
No Audits
b383e59aa162 fixed some latex; tried the alternative definition of Ramsey
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
9340467e8c9a Trying out Ramsey_eq for simpler proofs
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
54d98b691624 more tiny tweaks
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
0ace227c4d10 centralized more lemmas
Author
florian.haftmann
Browse Repository
No Builds
No Audits
aac14245270a avoid Fun.swap
Author
florian.haftmann
Browse Repository
No Builds
No Audits
3945ab3f00b8 guide is out of focus
Author
florian.haftmann
Browse Repository
No Builds
No Audits
c1ea0881dab4 Relational_Minimum_Spanning_Trees: refactoring Boruvka.thy
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
f8ded3c69c5d more elementary swap
Author
florian.haftmann
Browse Repository
No Builds
No Audits
3e3ac2ce9873 merged
Author
paulson
Browse Repository
No Builds
No Audits
9793065dd1c9 slight tidying of 1.19
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
718639187389 no hardwired document;
Author
makarius
Browse Repository
No Builds
No Audits
f9dd3b4a6fd5 tuned theory structure
Author
florian.haftmann
Browse Repository
No Builds
No Audits
c272e0d255f2 merged
Author
paulson
Browse Repository
No Builds
No Audits
5b179b8ac1fa more proof tidying
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
6cf5bfc61f4b collected lemmas on permutations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
30f9c323e6d0 merged
Author
paulson
Browse Repository
No Builds
No Audits
edae802b7d54 simpler proofs of stronger lemmas
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
15998112d738 just a few more tweaks
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
6a7d4e617b10 Tweaks
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
d119f1e8ad9a restructure proof
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
d217041e01ee tuned proofs
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
9ff0da80391b renamings
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
49921165cef0 lemma poly_asymp_equiv + simplified existing proof based on this lemma
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
f4ec023a9857 merged
Author
paulson
Browse Repository
No Builds
No Audits
67e4f5da18f4 some revisions to Lemma 3.7
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
8d3f34246608 Formatting, remove wrongly added file
Author
n.muendler <n.muendler@tum.de>
Browse Repository
No Builds
No Audits
943298de494d merged
Author
paulson
Browse Repository
No Builds
No Audits
e817fd6032e3 small refinements to partition proofs
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
6b5910524293 Add imperative deletion operation and OCaml code export to BTree entry
Author
n.muendler <n.muendler@tum.de>
Browse Repository
No Builds
No Audits
1edcb594d89c cleaning proofs, use more real_asymp
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits

Changes (174)

Path

Size

metadata/

templates/

BenOr_Kozen_Reif

BKR_Algorithm.thy

BKR_Decision.thy

Matrix_Equation_Construction.thy

More_Matrix.thy

Renegar_Algorithm.thy

Renegar_Decision.thy

Renegar_Proofs.thy

GaleStewart_Games

AlternatingLists.thy

FilteredList.thy

GaleStewartDefensiveStrategies.thy

GaleStewartDeterminedGames.thy

GaleStewartGames.thy

MoreCoinductiveList2.thy

Grothendieck_Schemes

Group_Extras.thy

Topological_Space.thy

Metalogic_ProofChecker

BetaNormProof.thy

EqualityProof.thy

EtaNormProof.thy

Preliminaries.thy

SortConstants.thy

Extended_Int.thy

Function_Ring.thy

Hensels_Lemma.thy

Padic_Construction.thy

Padic_Int_Polynomials.thy

Padic_Int_Topology.thy

Padic_Integers.thy

Supplementary_Ring_Facts.thy

Progress_Tracking

Exchange_Abadi.thy

Regression_Test_Selection

CollectionBasedRTS.thy

CollectionSemantics.thy

JVMCollectionBasedRTS.thy

JVMCollectionSemantics.thy

JVMSemantics.thy

ClassesAbove.thy

ClassesChanged.thy

JVMExecStepInductive.thy

Abstract_Completeness.html

Abstract_Soundness.html

Algebraic_Numbers.html

BNF_Operations.html

BenOr_Kozen_Reif.html

Berlekamp_Zassenhaus.html

Chandy_Lamport.html

Coinductive_Languages.html

Differential_Game_Logic.html

Dijkstra_Shortest_Path.html

Finger-Trees.html

Formula_Derivatives.html

Functional_Ordered_Resolution_Prover.html

GaleStewart_Games.html

Goedel_HFSet_Semantic.html

Goedel_HFSet_Semanticless.html

Goedel_Incompleteness.html

Grothendieck_Schemes.html

IFC_Tracking.html

Isabelle_Marries_Dirac.html

Jacobson_Basic_Algebra.html

LLL_Basis_Reduction.html

LLL_Factorization.html

LambdaAuth.html

List-Index.html

Localization_Ring.html

MFODL_Monitor_Optimized.html

MFOTL_Monitor.html

MSO_Regex_Equivalence.html

Metalogic_ProofChecker.html

Nested_Multisets_Ordinals.html

Ordered_Resolution_Prover.html

Padic_Ints.html

Parity_Game.html

Probabilistic_System_Zoo.html

Progress_Tracking.html

Projective_Geometry.html

Regex_Equivalence.html

Regression_Test_Selection.html

Robinson_Arithmetic.html

Sliding_Window_Algorithm.html

Sturm_Tarski.html

Subresultants.html

Syntax_Independent_Logic.html

statistics.html

rAFP17e46e9fdfda

metadata/metadata

Loading...

metadata/templates/about.tpl

Loading...

metadata/templates/using.tpl

Loading...

thys/BenOr_Kozen_Reif/BKR_Algorithm.thy

Loading...

thys/BenOr_Kozen_Reif/BKR_Decision.thy

Loading...

thys/BenOr_Kozen_Reif/BKR_Proofs.thy

Loading...

thys/BenOr_Kozen_Reif/Matrix_Equation_Construction.thy

Loading...

thys/BenOr_Kozen_Reif/More_Matrix.thy

Loading...

thys/BenOr_Kozen_Reif/ROOT

Loading...

thys/BenOr_Kozen_Reif/Renegar_Algorithm.thy

Loading...

thys/BenOr_Kozen_Reif/Renegar_Decision.thy

Loading...

thys/BenOr_Kozen_Reif/Renegar_Proofs.thy

Loading...

thys/BenOr_Kozen_Reif/document/root.bib

Loading...

thys/BenOr_Kozen_Reif/document/root.tex

Loading...

thys/GaleStewart_Games/AlternatingLists.thy

Loading...

thys/GaleStewart_Games/FilteredList.thy

Loading...

thys/GaleStewart_Games/GaleStewartDefensiveStrategies.thy

Loading...

thys/GaleStewart_Games/GaleStewartDeterminedGames.thy

Loading...

thys/GaleStewart_Games/GaleStewartGames.thy

Loading...

thys/GaleStewart_Games/MoreCoinductiveList2.thy

Loading...

thys/GaleStewart_Games/MoreENat.thy

Loading...

thys/GaleStewart_Games/MorePrefix.thy

Loading...

thys/GaleStewart_Games/ROOT

Loading...

thys/GaleStewart_Games/document/root.bib

Loading...

thys/GaleStewart_Games/document/root.tex

Loading...

thys/Grothendieck_Schemes/Comm_Ring.thy

Loading...

thys/Grothendieck_Schemes/Group_Extras.thy

Loading...

thys/Grothendieck_Schemes/ROOT

Loading...

thys/Grothendieck_Schemes/Scheme.thy

Loading...

thys/Grothendieck_Schemes/Set_Extras.thy

Loading...

thys/Grothendieck_Schemes/Topological_Space.thy

Loading...

thys/Grothendieck_Schemes/document/root.bib

Loading...

thys/Grothendieck_Schemes/document/root.tex

Loading...

thys/IFC_Tracking/IFC.thy

Loading...

thys/IFC_Tracking/PDG.thy

Loading...

thys/IFC_Tracking/ROOT

Loading...

thys/IFC_Tracking/document/root.bib

Loading...

thys/IFC_Tracking/document/root.tex

Loading...

thys/Metalogic_ProofChecker/BetaNorm.thy

Loading...

thys/Metalogic_ProofChecker/BetaNormProof.thy

Loading...

thys/Metalogic_ProofChecker/CheckerExe.thy

Loading...

thys/Metalogic_ProofChecker/CodeGen.thy

Loading...

thys/Metalogic_ProofChecker/Core.thy

Loading...

thys/Metalogic_ProofChecker/EqualityProof.thy

Loading...

thys/Metalogic_ProofChecker/EtaNorm.thy

Loading...

thys/Metalogic_ProofChecker/EtaNormProof.thy

Loading...

thys/Metalogic_ProofChecker/Instances.thy

Loading...

thys/Metalogic_ProofChecker/Logic.thy

Loading...

thys/Metalogic_ProofChecker/Name.thy

Loading...

thys/Metalogic_ProofChecker/Preliminaries.thy

Loading...

thys/Metalogic_ProofChecker/ProofTerm.thy

Loading...

thys/Metalogic_ProofChecker/ROOT

Loading...

thys/Metalogic_ProofChecker/SortConstants.thy

Loading...

thys/Metalogic_ProofChecker/Sorts.thy

Loading...

thys/Metalogic_ProofChecker/SortsExe.thy

Loading...

thys/Metalogic_ProofChecker/Term.thy

Loading...

thys/Metalogic_ProofChecker/Term_Subst.thy

Loading...

thys/Metalogic_ProofChecker/Theory.thy

Loading...

thys/Metalogic_ProofChecker/TheoryExe.thy

Loading...

thys/Metalogic_ProofChecker/document/root.bib

Loading...

thys/Metalogic_ProofChecker/document/root.tex

Loading...

thys/Padic_Ints/Cring_Poly.thy

Loading...

thys/Padic_Ints/Extended_Int.thy

Loading...

thys/Padic_Ints/Function_Ring.thy

Loading...

thys/Padic_Ints/Hensels_Lemma.thy

Loading...

thys/Padic_Ints/Padic_Construction.thy

Loading...

thys/Padic_Ints/Padic_Int_Polynomials.thy

Loading...

thys/Padic_Ints/Padic_Int_Topology.thy

Loading...

thys/Padic_Ints/Padic_Integers.thy

Loading...

thys/Padic_Ints/ROOT

Loading...

thys/Padic_Ints/Supplementary_Ring_Facts.thy

Loading...

thys/Padic_Ints/Zp_Compact.thy

Loading...

thys/Padic_Ints/document/root.bib

Loading...

thys/Padic_Ints/document/root.tex

Loading...

thys/Progress_Tracking/Antichain.thy

Loading...

thys/Progress_Tracking/Auxiliary.thy

Loading...

thys/Progress_Tracking/Combined.thy

Loading...

thys/Progress_Tracking/Exchange.thy

Loading...

thys/Progress_Tracking/Exchange_Abadi.thy

Loading...

thys/Progress_Tracking/Graph.thy

Loading...

thys/Progress_Tracking/Propagate.thy

Loading...

thys/Progress_Tracking/ROOT

Loading...

thys/Progress_Tracking/document/root.bib

Loading...

thys/Progress_Tracking/document/root.tex

Loading...

thys/ROOTS

Loading...

thys/Regression_Test_Selection/Common/CollectionBasedRTS.thy

Loading...

thys/Regression_Test_Selection/Common/CollectionSemantics.thy

Loading...

thys/Regression_Test_Selection/Common/RTS_safe.thy

Loading...

thys/Regression_Test_Selection/Common/Semantics.thy

Loading...

thys/Regression_Test_Selection/JVM_RTS/JVMCollectionBasedRTS.thy

Loading...

thys/Regression_Test_Selection/JVM_RTS/JVMCollectionSemantics.thy

Loading...

thys/Regression_Test_Selection/JVM_RTS/JVMSemantics.thy

Loading...

thys/Regression_Test_Selection/JinjaSuppl/ClassesAbove.thy

Loading...

thys/Regression_Test_Selection/JinjaSuppl/ClassesChanged.thy

Loading...

thys/Regression_Test_Selection/JinjaSuppl/JVMExecStepInductive.thy

Loading...

thys/Regression_Test_Selection/JinjaSuppl/Subcls.thy

Loading...

thys/Regression_Test_Selection/ROOT

Loading...

thys/Regression_Test_Selection/RTS.thy

Loading...

thys/Regression_Test_Selection/document/root.bib

Loading...

thys/Regression_Test_Selection/document/root.tex

Loading...

web/about.html

Loading...

web/entries/Abstract_Completeness.html

Loading...

web/entries/Abstract_Soundness.html

Loading...

web/entries/Algebraic_Numbers.html

Loading...

web/entries/BNF_Operations.html

Loading...

web/entries/BTree.html

Loading...

web/entries/BenOr_Kozen_Reif.html

Loading...

web/entries/Berlekamp_Zassenhaus.html

Loading...

web/entries/Chandy_Lamport.html

Loading...

web/entries/Coinductive_Languages.html

Loading...

web/entries/Differential_Game_Logic.html

Loading...

web/entries/Dijkstra_Shortest_Path.html

Loading...

web/entries/Finger-Trees.html

Loading...

web/entries/Formula_Derivatives.html

Loading...

web/entries/Functional_Ordered_Resolution_Prover.html

Loading...

web/entries/GaleStewart_Games.html

Loading...

web/entries/Goedel_HFSet_Semantic.html

Loading...

web/entries/Goedel_HFSet_Semanticless.html

Loading...

web/entries/Goedel_Incompleteness.html

Loading...

web/entries/Grothendieck_Schemes.html

Loading...

web/entries/IFC_Tracking.html

Loading...

web/entries/Isabelle_Marries_Dirac.html

Loading...

web/entries/Jacobson_Basic_Algebra.html

Loading...

web/entries/JinjaDCI.html

Loading...

web/entries/LLL_Basis_Reduction.html

Loading...

web/entries/LLL_Factorization.html

Loading...

web/entries/LambdaAuth.html

Loading...

web/entries/List-Index.html

Loading...

web/entries/Localization_Ring.html

Loading...

web/entries/MFODL_Monitor_Optimized.html

Loading...

web/entries/MFOTL_Monitor.html

Loading...

web/entries/MSO_Regex_Equivalence.html

Loading...

web/entries/Metalogic_ProofChecker.html

Loading...

web/entries/Nested_Multisets_Ordinals.html

Loading...

web/entries/Ordered_Resolution_Prover.html

Loading...

web/entries/Padic_Ints.html

Loading...

web/entries/Parity_Game.html

Loading...

web/entries/Probabilistic_System_Zoo.html

Loading...

web/entries/Progress_Tracking.html

Loading...

web/entries/Projective_Geometry.html

Loading...

web/entries/Regex_Equivalence.html

Loading...

web/entries/Regression_Test_Selection.html

Loading...

web/entries/Robinson_Arithmetic.html

Loading...

web/entries/Sliding_Window_Algorithm.html

Loading...

web/entries/Sturm_Tarski.html

Loading...

web/entries/Subresultants.html

Loading...

web/entries/Syntax_Independent_Logic.html

Loading...

web/index.html

Loading...

web/rss.xml

Loading...

web/statistics.html

Loading...

web/topics.html

Loading...

web/using.html

Loading...