Diffusion afp-devel b89191ec32d6

merge from afp-2021
b89191ec32d6
Actions

Description

merge from afp-2021

Details

Provenance

Andreas Lochbihler <mail@andreas-lochbihler.de>

Authored on

Parents

rAFPbde4cd3eb43d: sitegen for Registers
rAFP3a75f572994c: Correctness_Algebras: increase session timeout

Branches

Unknown

Tags

Unknown

Event Timeline

Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFPb89191ec32d6: merge from afp-2021.Nov 7 2021, 10:07 AM

Merged Changes

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

fa45268f13d7 tuned(afp/tools): tuned parser/unparser
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
88ca579ca6cd feat(afp/tools): more metadata and toml conversion;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
a3eb648b93ca feat(afp/tools): added TOML lexer and parser;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d6535281a69a tuned(afp/tools): module jar locations;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
3a75f572994c Correctness_Algebras: increase session timeout
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
49f5cc27cb2e tuned signature, according to Isabelle/df12779c3ce8;
Author
makarius
Browse Repository
No Builds
No Audits
b9fadc5d34c4 feat(SpecCheck) add possibility to make builds fail on failure and extend README
Author
kappelmann
Browse Repository
No Builds
No Audits
0b1dccde39f0 added missing funding information
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
b40b44b920f5 restored theory structure for simple genericity.
Author
florian.haftmann
Browse Repository
No Builds
No Audits
7825cfb5f214 Backed out changeset af549be0a8cd
Author
florian.haftmann
Browse Repository
No Builds
No Audits
af549be0a8cd restored different entrance points a before Isabelle2021
Author
florian.haftmann
Browse Repository
No Builds
No Audits
c3daa97ba53c proper parentheses (amending 354560d7143a);
Author
makarius
Browse Repository
No Builds
No Audits
ef2487130488 Adjusted to prospective release Isabelle2021-2.
Author
florian.haftmann
Browse Repository
No Builds
No Audits
cc4737a8a1ad Correctness_Algebras: uncomment counterexamples
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
ff251fab7614 clarified identity of theory data: avoid accidental pointer_eq, use equality on…
Author
makarius
Browse Repository
No Builds
No Audits
de5a2e151f8f clarified identity of theory data: pointer_eq is not well-defined (and fails on…
Author
makarius
Browse Repository
No Builds
No Audits
5a9bee294099 merge from afp-2021
Author
kleing
Browse Repository
No Builds
No Audits
f4d73fee73b5 adjust to isabelle@549019b4a808
Author
kleing
Browse Repository
No Builds
No Audits
2505f556a339 merge from afp-2021
Author
kleing
Browse Repository
No Builds
No Audits
e69dd05c4466 prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms;
Author
makarius
Browse Repository
No Builds
No Audits
807c0639d73d updated metadata for Count_Complex_Roots
Author
Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
Browse Repository
No Builds
No Audits
70ac60fa1e2d fix(afp/tools): added missing metadata, improved toml structure
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
49990125bc11 fix(afp/tools): removed TOML formatting heuristics for simplicity;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
88d0e6a26ce1 feat(afp/tools): added TOML module;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
02bc4563612a feat(afp/tools): added metadata migration tool;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
12c42ff80fc6 feat(afp/tools): migrated scala tool_bodys to proper tools;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
fe3f71f31996 corrected the timeout for CZH_Universal_Constructions
Author
user9716869 <user9716869@gmail.com>
Browse Repository
No Builds
No Audits
fee517746747 CZH: further results about comma categories and Kan extensions, a variety of…
Author
user9716869 <user9716869@gmail.com>
Browse Repository
No Builds
No Audits
99b814982902 more generic bit/word lemmas for distribution
Author
florian.haftmann
Browse Repository
No Builds
No Audits
1d43ab62d7eb Fixing a name clash between two different "restrict" operators
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
bddb42d8c62a Merged
Author
Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
Browse Repository
No Builds
No Audits
82a159e398cf solved the roots-on-the-border problem
Author
Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
Browse Repository
No Builds
No Audits
cb70e6f97bfa split Count_Complex_Roots
Author
Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
Browse Repository
No Builds
No Audits
b8642e91d99f more realistic timeout;
Author
makarius
Browse Repository
No Builds
No Audits
55910792390b clarified signature, according to Isabelle/ccf599864beb;
Author
makarius
Browse Repository
No Builds
No Audits
b7f45664e583 back to dedicated separate shift operations for infix syntax;
Author
florian.haftmann
Browse Repository
No Builds
No Audits
802a16fc10b0 modify JinjaDCI
Author
nanjiang <nanjiang@whu.edu.cn>
Browse Repository
No Builds
No Audits
c5336131e4b5 modify JinjaDCI
Author
nanjiang <nanjiang@whu.edu.cn>
Browse Repository
No Builds
No Audits
e11414b94aae Merged.
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
838fe8a9a303 Various tuning that for some reason didn't get merged from my master branch.
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
d4f54c2a05d1 A spot of polishing
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
16f5e2769f1b Merged.
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
e8939a7952f7 Update metadata to reflect changes made in July, 2021.
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
214d269370b1 Add a revision note concerning material added in July, 2021.
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
5fee9e3ac452 tuned signature, according to Isabelle/042041c0ebeb;
Author
makarius
Browse Repository
No Builds
No Audits
5a88b16092a6 Merged.
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
1943b411fa58 Sync with my development repo.
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
7a7605e22a07 Adjust Imperative List/Map/Set Specification for more lenient next operation
Author
n.muendler <n.muendler@tum.de>
Browse Repository
No Builds
No Audits
f879f9b59107 discontinued obsolete "val extend = I" for data slots;
Author
makarius
Browse Repository
No Builds
No Audits
96076d0d60c2 tuned;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (38)

Path

Size

metadata/

Axioms_Complement.thy

Axioms_Complement_Quantum.thy

Axioms_Quantum.thy

Classical_Extra.thy

Finite_Tensor_Product.thy

Finite_Tensor_Product_Matrices.thy

Laws_Complement_Quantum.thy

Complex_Bounded_Operators.html

rAFPb89191ec32d6

View Options

metadata/metadata

View Options

thys/ROOTS

View Options

thys/Registers/Axioms.thy

View Options

thys/Registers/Axioms_Classical.thy

View Options

thys/Registers/Axioms_Complement.thy

View Options

thys/Registers/Axioms_Complement_Quantum.thy

View Options

thys/Registers/Axioms_Quantum.thy

View Options

thys/Registers/Classical_Extra.thy

View Options

thys/Registers/Finite_Tensor_Product.thy

View Options

thys/Registers/Finite_Tensor_Product_Matrices.thy

View Options

thys/Registers/LICENSE

View Options

thys/Registers/Laws.thy

View Options

thys/Registers/Laws_Classical.thy

View Options

thys/Registers/Laws_Complement.thy

View Options

thys/Registers/Laws_Complement_Quantum.thy

View Options

thys/Registers/Laws_Quantum.thy

View Options

thys/Registers/Misc.thy

View Options

thys/Registers/Pure_States.thy

View Options

thys/Registers/QHoare.thy

View Options

thys/Registers/Quantum.thy

View Options

thys/Registers/Quantum_Extra.thy

View Options

thys/Registers/Quantum_Extra2.thy

View Options

thys/Registers/ROOT

View Options

thys/Registers/Teleport.thy

View Options

thys/Registers/document/root.bib

View Options

thys/Registers/document/root.tex

View Options

thys/Registers/instantiate_laws.py

View Options

web/entries/Complex_Bounded_Operators.html

View Options

web/entries/Registers.html

View Options

web/index.html

View Options

web/rss.xml

View Options

web/statistics.html

View Options

merge from afp-2021b89191ec32d6Actions

Description

Details

Event Timeline

Merged Changes

Changes (38)

rAFPb89191ec32d6

metadata/metadata

thys/ROOTS

thys/Registers/Axioms.thy

thys/Registers/Axioms_Classical.thy

thys/Registers/Axioms_Complement.thy

thys/Registers/Axioms_Complement_Quantum.thy

thys/Registers/Axioms_Quantum.thy

thys/Registers/Classical_Extra.thy

thys/Registers/Finite_Tensor_Product.thy

thys/Registers/Finite_Tensor_Product_Matrices.thy

thys/Registers/LICENSE

thys/Registers/Laws.thy

thys/Registers/Laws_Classical.thy

thys/Registers/Laws_Complement.thy

thys/Registers/Laws_Complement_Quantum.thy

thys/Registers/Laws_Quantum.thy

thys/Registers/Misc.thy

thys/Registers/Pure_States.thy

thys/Registers/QHoare.thy

thys/Registers/Quantum.thy

thys/Registers/Quantum_Extra.thy

thys/Registers/Quantum_Extra2.thy

thys/Registers/ROOT

thys/Registers/Teleport.thy

thys/Registers/document/root.bib

thys/Registers/document/root.tex

thys/Registers/instantiate_laws.py

web/entries/Complex_Bounded_Operators.html

web/entries/Registers.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html

merge from afp-2021
b89191ec32d6
Actions