Diffusion afp-devel 621bc6675749

merge from afp-2021-1
621bc6675749
Actions

Tags

None

Subscribers

None

Description

merge from afp-2021-1

Details

Provenance

Authored on

Parents

rAFP6486ab915f12: new entry: Nano_JSON
rAFP4b70dbdbeea7: merged

Branches

Unknown

Tags

Unknown

Event Timeline

kleing committed rAFP621bc6675749: merge from afp-2021-1.Aug 23 2022, 9:28 AM

Merged Changes

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

4b70dbdbeea7 merged
Author
makarius
Browse Repository
No Builds
No Audits
c8deb994f6e9 Isabelle/b6589c8ccadd officially supports README.thy;
Author
makarius
Browse Repository
No Builds
No Audits
59b0a80cf40b streamlined
Author
florian.haftmann
Browse Repository
No Builds
No Audits
26a20c98b97c tuned proofs
Author
florian.haftmann
Browse Repository
No Builds
No Audits
561d723d6358 discontinued obsolete README.html: superseded by abstract provided by AFP;
Author
makarius
Browse Repository
No Builds
No Audits
3d7eaa9f630e streamlined primitive definitions for integer division
Author
florian.haftmann
Browse Repository
No Builds
No Audits
d186b2e87e18 tuned code equations for Xml-parsing
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
56991031ffef refactored algebraic number theories, generalized Cauchy Root Bounds lemma (so…
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
fea99b2f42bf Revision of locale structure
Author
sterraf
Browse Repository
No Builds
No Audits
5d66d61cbd52 Purely markup
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
22f95a29b159 Fix ImpSplit thy for document generation
Author
Niels Mündler <n.muendler@web.de>
Browse Repository
No Builds
No Audits
b5b59c822549 Add B+Tree formalisation to the BTree entry
Author
Niels Mündler <n.muendler@web.de>
Browse Repository
No Builds
No Audits
c4f6f33e7466 Correcting thm antiquotations. Turning code comments into text
Author
sterraf
Browse Repository
No Builds
No Audits
7dacd5f58334 Update metadata and root.tex to mention the addition of ZFC_SetCat in early…
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
8190a9ebc716 Sync with my development repo: Category3: add various rules for limits. RTS…
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
56d5a40ba8fc adapted to NLists.thy
Author
nipkow
Browse Repository
No Builds
No Audits
64e1c7e89ad3 merged
Author
nipkow
Browse Repository
No Builds
No Audits
965b1fce10d0 use Library/NList.thy now
Author
nipkow
Browse Repository
No Builds
No Audits
eca5cf0e4817 Further streamlining of quick-and-dirty evaluation.
Author
florian.haftmann
Browse Repository
No Builds
No Audits
cabf521b7579 An attempt for an integrated solution for quick-and-dirty evaluation.
Author
florian.haftmann
Browse Repository
No Builds
No Audits
a0a812d549dd Further reduction of locale assumptions
Author
sterraf
Browse Repository
No Builds
No Audits
41e138072234 merged
Author
makarius
Browse Repository
No Builds
No Audits
3bf5b42fa409 more complete theorem_commands;
Author
makarius
Browse Repository
No Builds
No Audits
c42f49b4cb14 clarified signature, following Isabelle/b6d74c90b588;
Author
makarius
Browse Repository
No Builds
No Audits
f442b8a512de Update metadata for Frequency_Moments.
Author
Emin Karayel <me@eminkarayel.de>
Browse Repository
No Builds
No Audits
dffbafe5983e merged
Author
Richard Schmoetten <richard.schmoetten@ed.ac.uk>
Browse Repository
No Builds
No Audits
ff8762a1868c Update Schutz_Spacetime
Author
Richard Schmoetten <richard.schmoetten@ed.ac.uk>
Browse Repository
No Builds
No Audits
855e895beb9c more accurate name
Author
blanchette
Browse Repository
No Builds
No Audits
04bb771f4700 more politically correct
Author
blanchette
Browse Repository
No Builds
No Audits
154dc66d9621 two new lemmas
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
1e9471f837af added two lemmas to relational chains
Author
blanchette
Browse Repository
No Builds
No Audits
f78309f3fd50 changed confusing assumption name
Author
blanchette
Browse Repository
No Builds
No Audits
126a0ee1b713 avoid the surprise that n-m is 0 even if n<m.
Author
nipkow
Browse Repository
No Builds
No Audits
3ba39711b355 tuned
Author
nipkow
Browse Repository
No Builds
No Audits
fc50c0c63ef5 simplified invar
Author
nipkow
Browse Repository
No Builds
No Audits
6d0ba027f706 merged
Author
nipkow
Browse Repository
No Builds
No Audits
ba8ca176ff4c simplified
Author
nipkow
Browse Repository
No Builds
No Audits
e663830ac9ed update metadata;
Author
makarius
Browse Repository
No Builds
No Audits
7a3e6e182e9d merged
Author
nipkow
Browse Repository
No Builds
No Audits
8cc1bff9db10 tuned
Author
nipkow
Browse Repository
No Builds
No Audits
9663b335a71e removed a spurious locale parameter -- the same issue probably arises in the…
Author
blanchette
Browse Repository
No Builds
No Audits
8f58103dc2d4 removed needless assumption
Author
blanchette
Browse Repository
No Builds
No Audits
f307ca3c67f0 Named intermediate results combinable wands
Author
Thibault Dardinier <thibault.dardinier@inf.ethz.ch>
Browse Repository
No Builds
No Audits
d0222e3a4c4c Named intermediate results Package logic
Author
Thibault Dardinier <thibault.dardinier@inf.ethz.ch>
Browse Repository
No Builds
No Audits
3488d4772567 added lemma about lazy list chains
Author
blanchette
Browse Repository
No Builds
No Audits
0ab6087cd196 typo
Author
blanchette
Browse Repository
No Builds
No Audits
d1cdfc97ad72 Refining three sessions.
Author
sterraf
Browse Repository
No Builds
No Audits
206c4f90ab7c Tuned.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
8100a56c7055 merged
Author
nipkow
Browse Repository
No Builds
No Audits
bbb083f81730 addd DOIs and other metadata links
Author
nipkow
Browse Repository
No Builds
No Audits

Changes (189)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

Commuting_Hermitian.toml

Involutions2Squares.toml

Commuting_Hermitian

Commuting_Hermitian.thy

Commuting_Hermitian_Misc.thy

Spectral_Theory_Complements.thy

AdaptiveStateCounting

Adaptive_Test_Case.thy

Backwards_Reachability_Analysis.thy

Helper_Algorithms.thy

Maximal_Path_Trie.thy

R_Distinguishability.thy

State_Preamble.thy

State_Separator.thy

Test_Suite_Calculation.thy

Test_Suite_Calculation_Refined.thy

Test_Suite_IO.thy

Traversal_Set.thy

Distinguishability.thy

EquivalenceTesting

Convergence.thy

Convergence_Graph.thy

Empty_Convergence_Graph.thy

HSI_Method_Implementations.thy

H_Framework.thy

H_Method_Implementations.thy

Intermediate_Frameworks.thy

Intermediate_Implementations.thy

Pair_Framework.thy

Partial_S_Method_Implementations.thy

SPYH_Method_Implementations.thy

SPY_Framework.thy

SPY_Method_Implementations.thy

Simple_Convergence_Graph.thy

Simple_Convergence_Graph_Trie.thy

Test_Suite_Representations.thy

Test_Suite_Representations_Refined.thy

W_Method_Implementations.thy

Wp_Method_Implementations.thy

FSM_Code_Datatype.thy

IO_Sequence_Set.thy

Minimisation.thy

OFSM_Tables_Refined.thy

Observability.thy

Prefix_Tree.thy

Prefix_Tree_Refined.thy

Prime_Transformation.thy

Product_FSM.thy

State_Cover.thy

Test_Suite_Generator_Code_Export.thy

Util_Refined.thy

Involutions2Squares

Involutions2Squares.thy

Example_Real.thy

Nano_JSON_Lexer.ML

Nano_JSON_Main.thy

Nano_JSON_Manual.thy

Nano_JSON_Parser.ML

Nano_JSON_Query.ML

Nano_JSON_Query.thy

Nano_JSON_Serializer.ML

Nano_JSON_Type.ML

Compile_Evaluator.thy

Constant_Folding.thy

Environment.thy

Solidity_Evaluator.thy

Solidity_Main.thy

Solidity_Symbex.thy

authors/

bortin/

brucker/

echenim/

marmsoler/

sachtleben/

data/

containers/

datatype_order_generator/

native_word/

projective_measurements

Adaptive_State_Counting.html

Commuting_Hermitian.html

Containers.html

Datatype_Order_Generator.html

EdmondsKarp_Maxflow.html

Flow_Networks.html

Involutions2Squares.html

Native_Word.html

Projective_Measurements.html

Prpu_Maxflow.html

statistics/

commuting_hermitian

involutions2squares

topics/

computer-science/

algorithms/

automata-and-formal-languages/

data-structures/

programming-languages/

semantics-and-reasoning/

mathematics/

algebra/

number-theory/

tools/

rAFP621bc6675749

metadata/authors.toml

metadata/entries/Commuting_Hermitian.toml

metadata/entries/FSM_Tests.toml

metadata/entries/Involutions2Squares.toml

metadata/entries/Nano_JSON.toml

metadata/entries/Solidity.toml

thys/Commuting_Hermitian/Commuting_Hermitian.thy

thys/Commuting_Hermitian/Commuting_Hermitian_Misc.thy

thys/Commuting_Hermitian/ROOT

thys/Commuting_Hermitian/Spectral_Theory_Complements.thy

thys/Commuting_Hermitian/document/root.tex

thys/FSM_Tests/AdaptiveStateCounting/Adaptive_Test_Case.thy

thys/FSM_Tests/AdaptiveStateCounting/Backwards_Reachability_Analysis.thy

thys/FSM_Tests/AdaptiveStateCounting/Helper_Algorithms.thy

thys/FSM_Tests/AdaptiveStateCounting/Maximal_Path_Trie.thy

thys/FSM_Tests/AdaptiveStateCounting/R_Distinguishability.thy

thys/FSM_Tests/AdaptiveStateCounting/State_Preamble.thy

thys/FSM_Tests/AdaptiveStateCounting/State_Separator.thy

thys/FSM_Tests/AdaptiveStateCounting/Test_Suite.thy

thys/FSM_Tests/AdaptiveStateCounting/Test_Suite_Calculation.thy

thys/FSM_Tests/AdaptiveStateCounting/Test_Suite_Calculation_Refined.thy

thys/FSM_Tests/AdaptiveStateCounting/Test_Suite_IO.thy

thys/FSM_Tests/AdaptiveStateCounting/Traversal_Set.thy

thys/FSM_Tests/Distinguishability.thy

thys/FSM_Tests/EquivalenceTesting/Convergence.thy

thys/FSM_Tests/EquivalenceTesting/Convergence_Graph.thy

thys/FSM_Tests/EquivalenceTesting/Empty_Convergence_Graph.thy

thys/FSM_Tests/EquivalenceTesting/HSI_Method_Implementations.thy

thys/FSM_Tests/EquivalenceTesting/H_Framework.thy

thys/FSM_Tests/EquivalenceTesting/H_Method_Implementations.thy

thys/FSM_Tests/EquivalenceTesting/Intermediate_Frameworks.thy

thys/FSM_Tests/EquivalenceTesting/Intermediate_Implementations.thy

thys/FSM_Tests/EquivalenceTesting/Pair_Framework.thy

thys/FSM_Tests/EquivalenceTesting/Partial_S_Method_Implementations.thy

thys/FSM_Tests/EquivalenceTesting/SPYH_Method_Implementations.thy

thys/FSM_Tests/EquivalenceTesting/SPY_Framework.thy

thys/FSM_Tests/EquivalenceTesting/SPY_Method_Implementations.thy

thys/FSM_Tests/EquivalenceTesting/Simple_Convergence_Graph.thy

thys/FSM_Tests/EquivalenceTesting/Simple_Convergence_Graph_Trie.thy

thys/FSM_Tests/EquivalenceTesting/Test_Suite_Representations.thy

thys/FSM_Tests/EquivalenceTesting/Test_Suite_Representations_Refined.thy

thys/FSM_Tests/EquivalenceTesting/W_Method_Implementations.thy

thys/FSM_Tests/EquivalenceTesting/Wp_Method_Implementations.thy

thys/FSM_Tests/FSM.thy

thys/FSM_Tests/FSM_Code_Datatype.thy

thys/FSM_Tests/FSM_Impl.thy

thys/FSM_Tests/IO_Sequence_Set.thy

thys/FSM_Tests/Minimisation.thy

thys/FSM_Tests/OFSM_Tables_Refined.thy

thys/FSM_Tests/Observability.thy

thys/FSM_Tests/Prefix_Tree.thy

thys/FSM_Tests/Prefix_Tree_Refined.thy

thys/FSM_Tests/Prime_Transformation.thy

thys/FSM_Tests/Product_FSM.thy

thys/FSM_Tests/ROOT

thys/FSM_Tests/State_Cover.thy

thys/FSM_Tests/Test_Suite_Generator_Code_Export.thy

thys/FSM_Tests/Util.thy

thys/FSM_Tests/Util_Refined.thy

thys/FSM_Tests/document/root.bib

thys/FSM_Tests/document/root.tex

thys/Involutions2Squares/Involutions2Squares.thy

thys/Involutions2Squares/ROOT

thys/Involutions2Squares/document/root.tex

thys/Nano_JSON/Example.thy

thys/Nano_JSON/Example_Real.thy

thys/Nano_JSON/Nano_JSON.thy

thys/Nano_JSON/Nano_JSON_Lexer.ML

thys/Nano_JSON/Nano_JSON_Main.thy

thys/Nano_JSON/Nano_JSON_Manual.thy

thys/Nano_JSON/Nano_JSON_Parser.ML

thys/Nano_JSON/Nano_JSON_Query.ML

thys/Nano_JSON/Nano_JSON_Query.thy

thys/Nano_JSON/Nano_JSON_Serializer.ML

thys/Nano_JSON/Nano_JSON_Type.ML

thys/Nano_JSON/ROOT

thys/Nano_JSON/document/orcidlink.sty

thys/Nano_JSON/document/root.bib

thys/Nano_JSON/document/root.tex

thys/Nano_JSON/example.json

thys/ROOTS

thys/Solidity/Accounts.thy

thys/Solidity/Compile_Evaluator.thy

thys/Solidity/Constant_Folding.thy

thys/Solidity/Environment.thy

thys/Solidity/ROOT

thys/Solidity/ReadShow.thy

thys/Solidity/Reentrancy.thy

thys/Solidity/Solidity_Evaluator.thy

thys/Solidity/Solidity_Main.thy

thys/Solidity/Solidity_Symbex.thy

thys/Solidity/StateMonad.thy

thys/Solidity/Statements.thy

thys/Solidity/Storage.thy

thys/Solidity/Valuetypes.thy

thys/Solidity/document/orcidlink.sty

thys/Solidity/document/root.bib

thys/Solidity/document/root.tex

web/authors/bortin/index.html

web/authors/bortin/index.xml

web/authors/brucker/index.html

web/authors/brucker/index.xml

web/authors/echenim/index.html

web/authors/echenim/index.xml

web/authors/marmsoler/index.html

web/authors/marmsoler/index.xml

web/authors/sachtleben/index.html

web/authors/sachtleben/index.xml

web/data/keywords.json

web/dependencies/containers/index.html

web/dependencies/containers/index.xml

web/dependencies/datatype_order_generator/index.html

web/dependencies/datatype_order_generator/index.xml

web/dependencies/index.html

web/dependencies/index.json

web/dependencies/native_word/index.html

web/dependencies/native_word/index.xml

web/dependencies/projective_measurements/index.html

web/dependencies/projective_measurements/index.xml

web/entries/Adaptive_State_Counting.html

web/entries/BTree.html

web/entries/Commuting_Hermitian.html

web/entries/Containers.html

web/entries/Datatype_Order_Generator.html

web/entries/EdmondsKarp_Maxflow.html

web/entries/FSM_Tests.html

web/entries/Flow_Networks.html

web/entries/Involutions2Squares.html

web/entries/JinjaDCI.html

web/entries/Nano_JSON.html

web/entries/Native_Word.html

web/entries/Projective_Measurements.html

web/entries/Prpu_Maxflow.html

web/entries/Solidity.html

web/entries/index.html

web/entries/index.xml

web/index.html

web/index.json

web/index.xml

web/sitemap.xml

web/statistics/index.html

web/theories/commuting_hermitian/index.html

web/theories/fsm_tests/index.html

web/theories/index.xml

web/theories/involutions2squares/index.html

web/theories/nano_json/index.html

web/theories/solidity/index.html

web/topics/computer-science/algorithms/index.html

web/topics/computer-science/algorithms/index.xml

web/topics/computer-science/automata-and-formal-languages/index.html

web/topics/computer-science/automata-and-formal-languages/index.xml

web/topics/computer-science/data-structures/index.html

web/topics/computer-science/data-structures/index.xml

web/topics/computer-science/programming-languages/index.html

web/topics/computer-science/programming-languages/index.xml

web/topics/computer-science/semantics-and-reasoning/index.html

web/topics/computer-science/semantics-and-reasoning/index.xml

web/topics/index.html

web/topics/mathematics/algebra/index.html

web/topics/mathematics/algebra/index.xml

web/topics/mathematics/number-theory/index.html

web/topics/mathematics/number-theory/index.xml

web/topics/tools/index.html

web/topics/tools/index.xml