Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. Eliminated the temporary material that was already migrated to the Isabelle libraries
  2. merge from afp-2021-1
  3. regenerate site;
  4. tuned;
  5. merged
  6. New entry CRYSTALS-Kyber
  7. regenerate site;
  8. added missing history in metadata;
  9. retrieve missing change history in metadata migration tool;
  10. backout b2ae7c2c3ea51af8f43b76cdcb5d499c5085e726
  11. new email address for Maksym
  12. metadata and sitegen for Khovansikii_Theorem
  13. new entry: Khovanski-Theorem
  14. fixed metadata for Hales_Jewett
  15. sitegen for Number_Theoretic_Transform
  16. new entry Number_Theoretic_Transform
  17. new entry Hales Jewett
  18. adapt to only check ROOT for directories in thys (aftermath of Isabelle/a9bbf075f4319e920a22a1c0a5b763b6575f2089);
Changeset 12993:4bdd34701622 by paulson _lp15@cam.ac.uk_:
Eliminated the temporary material that was already migrated to the Isabelle libraries
The file was modified thys/Khovanskii_Theorem/Khovanskii.thy
The file was removedthys/Khovanskii_Theorem/For_2022.thy
Changeset 12992:2752cd0567c9 by fabian huch _huch@in.tum.de_:
merge from afp-2021-1
Changeset 12991:2011079530c4 by fabian huch _huch@in.tum.de_:
regenerate site;
The file was modified web/entries/Affine_Arithmetic.html
The file was modified web/entries/Algebraic_Numbers.html
The file was modified web/entries/Amortized_Complexity.html
The file was modified web/entries/Applicative_Lifting.html
The file was modified web/entries/Approximation_Algorithms.html
The file was modified web/entries/Architectural_Design_Patterns.html
The file was modified web/entries/Collections.html
The file was modified web/entries/Containers.html
The file was modified web/entries/Efficient-Mergesort.html
The file was modified web/entries/Flyspeck-Tame.html
The file was modified web/entries/Interpreter_Optimizations.html
The file was modified web/entries/Jordan_Normal_Form.html
The file was modified web/entries/LLL_Basis_Reduction.html
The file was modified web/entries/LTL_to_DRA.html
The file was modified web/entries/Launchbury.html
The file was modified web/entries/Native_Word.html
The file was modified web/entries/Ordinary_Differential_Equations.html
The file was modified web/entries/Polynomials.html
The file was modified web/entries/Regular-Sets.html
The file was modified web/entries/Resolution_FOL.html
The file was modified web/entries/Show.html
The file was modified web/entries/Sqrt_Babylonian.html
The file was modified web/entries/Well_Quasi_Orders.html
Changeset 12990:6d58e998e657 by fabian huch _huch@in.tum.de_:
tuned;
The file was modified metadata/entries/Affine_Arithmetic.toml
The file was modified metadata/entries/Algebraic_Numbers.toml
The file was modified metadata/entries/Amortized_Complexity.toml
The file was modified metadata/entries/Applicative_Lifting.toml
The file was modified metadata/entries/Approximation_Algorithms.toml
The file was modified metadata/entries/Architectural_Design_Patterns.toml
The file was modified metadata/entries/Collections.toml
The file was modified metadata/entries/Containers.toml
The file was modified metadata/entries/Efficient-Mergesort.toml
The file was modified metadata/entries/Flyspeck-Tame.toml
The file was modified metadata/entries/Interpreter_Optimizations.toml
The file was modified metadata/entries/Jordan_Normal_Form.toml
The file was modified metadata/entries/LLL_Basis_Reduction.toml
The file was modified metadata/entries/LTL_to_DRA.toml
The file was modified metadata/entries/Launchbury.toml
The file was modified metadata/entries/Native_Word.toml
The file was modified metadata/entries/Ordinary_Differential_Equations.toml
The file was modified metadata/entries/Polynomials.toml
The file was modified metadata/entries/Regular-Sets.toml
The file was modified metadata/entries/Resolution_FOL.toml
The file was modified metadata/entries/Show.toml
The file was modified metadata/entries/Sqrt_Babylonian.toml
The file was modified metadata/entries/Well_Quasi_Orders.toml
Changeset 12989:72772a622eb3 by paulson:
merged
Changeset 12988:11a3d3871dea by paulson _lp15@cam.ac.uk_:
New entry CRYSTALS-Kyber
The file was addedmetadata/entries/CRYSTALS-Kyber.toml
The file was addedthys/CRYSTALS-Kyber/Abs_Qr.thy
The file was addedthys/CRYSTALS-Kyber/Compress.thy
The file was addedthys/CRYSTALS-Kyber/Crypto_Scheme.thy
The file was addedthys/CRYSTALS-Kyber/Crypto_Scheme_NTT.thy
The file was addedthys/CRYSTALS-Kyber/Kyber_NTT_Values.thy
The file was addedthys/CRYSTALS-Kyber/Kyber_Values.thy
The file was addedthys/CRYSTALS-Kyber/Kyber_spec.thy
The file was addedthys/CRYSTALS-Kyber/Mod_Plus_Minus.thy
The file was addedthys/CRYSTALS-Kyber/Mod_Ring_Numeral.thy
The file was addedthys/CRYSTALS-Kyber/NTT_Scheme.thy
The file was addedthys/CRYSTALS-Kyber/Powers3844.thy
The file was addedthys/CRYSTALS-Kyber/ROOT
The file was addedthys/CRYSTALS-Kyber/document/root.bib
The file was addedthys/CRYSTALS-Kyber/document/root.tex
The file was addedweb/dependencies/number_theoretic_transform/index.html
The file was addedweb/dependencies/number_theoretic_transform/index.xml
The file was addedweb/entries/CRYSTALS-Kyber.html
The file was addedweb/theories/crystals-kyber/index.html
The file was modified thys/ROOTS
The file was modified web/authors/kreuzer/index.html
The file was modified web/authors/kreuzer/index.xml
The file was modified web/data/keywords.json
The file was modified web/dependencies/berlekamp_zassenhaus/index.html
The file was modified web/dependencies/berlekamp_zassenhaus/index.xml
The file was modified web/dependencies/index.html
The file was modified web/dependencies/index.json
The file was modified web/entries/Berlekamp_Zassenhaus.html
The file was modified web/entries/Number_Theoretic_Transform.html
The file was modified web/entries/index.html
The file was modified web/entries/index.xml
The file was modified web/index.html
The file was modified web/index.json
The file was modified web/index.xml
The file was modified web/sitemap.xml
The file was modified web/statistics/index.html
The file was modified web/theories/index.xml
The file was modified web/topics/computer-science/security/index.html
The file was modified web/topics/computer-science/security/index.xml
The file was modified web/topics/index.html
Changeset 12987:afc81491665d by fabian huch _huch@in.tum.de_:
regenerate site;
The file was modified web/entries/Aggregation_Algebras.html
The file was modified web/entries/Applicative_Lifting.html
The file was modified web/entries/Approximation_Algorithms.html
The file was modified web/entries/BTree.html
The file was modified web/entries/Bicategory.html
The file was modified web/entries/Bounded_Deducibility_Security.html
The file was modified web/entries/Category3.html
The file was modified web/entries/Coinductive.html
The file was modified web/entries/Complx.html
The file was modified web/entries/Containers.html
The file was modified web/entries/Dependent_SIFUM_Refinement.html
The file was modified web/entries/Dependent_SIFUM_Type_Systems.html
The file was modified web/entries/DiscretePricing.html
The file was modified web/entries/Efficient-Mergesort.html
The file was modified web/entries/Featherweight_OCL.html
The file was modified web/entries/FinFun.html
The file was modified web/entries/Game_Based_Crypto.html
The file was modified web/entries/GewirthPGCProof.html
The file was modified web/entries/JinjaThreads.html
The file was modified web/entries/LTL.html
The file was modified web/entries/MFMC_Countable.html
The file was modified web/entries/MFOTL_Monitor.html
The file was modified web/entries/Modal_Logics_for_NTS.html
The file was modified web/entries/MonoidalCategory.html
The file was modified web/entries/Monomorphic_Monad.html
The file was modified web/entries/Native_Word.html
The file was modified web/entries/Network_Security_Policy_Verification.html
The file was modified web/entries/Optics.html
The file was modified web/entries/Perron_Frobenius.html
The file was modified web/entries/Probabilistic_While.html
The file was modified web/entries/Relational_Disjoint_Set_Forests.html
The file was modified web/entries/Stone_Relation_Algebras.html
The file was modified web/entries/Szpilrajn.html
Changeset 12986:791a909ac26e by fabian huch _huch@in.tum.de_:
added missing history in metadata;
The file was modified metadata/entries/Aggregation_Algebras.toml
The file was modified metadata/entries/Applicative_Lifting.toml
The file was modified metadata/entries/Approximation_Algorithms.toml
The file was modified metadata/entries/BTree.toml
The file was modified metadata/entries/Bicategory.toml
The file was modified metadata/entries/Bounded_Deducibility_Security.toml
The file was modified metadata/entries/Category3.toml
The file was modified metadata/entries/Coinductive.toml
The file was modified metadata/entries/Complx.toml
The file was modified metadata/entries/Containers.toml
The file was modified metadata/entries/Dependent_SIFUM_Refinement.toml
The file was modified metadata/entries/Dependent_SIFUM_Type_Systems.toml
The file was modified metadata/entries/DiscretePricing.toml
The file was modified metadata/entries/Efficient-Mergesort.toml
The file was modified metadata/entries/Featherweight_OCL.toml
The file was modified metadata/entries/FinFun.toml
The file was modified metadata/entries/Game_Based_Crypto.toml
The file was modified metadata/entries/GewirthPGCProof.toml
The file was modified metadata/entries/JinjaThreads.toml
The file was modified metadata/entries/LTL.toml
The file was modified metadata/entries/MFMC_Countable.toml
The file was modified metadata/entries/MFOTL_Monitor.toml
The file was modified metadata/entries/Modal_Logics_for_NTS.toml
The file was modified metadata/entries/MonoidalCategory.toml
The file was modified metadata/entries/Monomorphic_Monad.toml
The file was modified metadata/entries/Native_Word.toml
The file was modified metadata/entries/Network_Security_Policy_Verification.toml
The file was modified metadata/entries/Optics.toml
The file was modified metadata/entries/Perron_Frobenius.toml
The file was modified metadata/entries/Probabilistic_While.toml
The file was modified metadata/entries/Relational_Disjoint_Set_Forests.toml
The file was modified metadata/entries/Stone_Relation_Algebras.toml
The file was modified metadata/entries/Szpilrajn.toml
Changeset 12985:ac2b59b37741 by fabian huch _huch@in.tum.de_:
retrieve missing change history in metadata migration tool;
The file was modified tools/migration/afp_migrate_metadata.scala
Changeset 12984:490d1fdcd266 by fabian huch _huch@in.tum.de_:
backout b2ae7c2c3ea51af8f43b76cdcb5d499c5085e726
The file was addedtools/migration/afp_migrate_metadata.scala
The file was addedtools/migration/public_suffix_list.dat
The file was modified etc/build.props
The file was modified tools/afp_tool.scala
Changeset 12983:457e3b13987e by gerwin klein _kleing@unsw.edu.au_:
new email address for Maksym
The file was modified metadata/authors.toml
The file was modified metadata/entries/Involutions2Squares.toml
The file was modified web/authors/bortin/index.html
The file was modified web/entries/Involutions2Squares.html
Changeset 12982:e91943d681a1 by rene thiemann _rene.thiemann@uibk.ac.at_:
metadata and sitegen for Khovansikii_Theorem
The file was addedmetadata/entries/Khovanskii_Theorem.toml
The file was addedweb/dependencies/pluennecke_ruzsa_inequality/index.html
The file was addedweb/dependencies/pluennecke_ruzsa_inequality/index.xml
The file was addedweb/entries/Khovanskii_Theorem.html
The file was addedweb/theories/khovanskii_theorem/index.html
The file was modified web/authors/argyraki/index.html
The file was modified web/authors/argyraki/index.xml
The file was modified web/authors/eberl/index.html
The file was modified web/authors/eberl/index.xml
The file was modified web/authors/kreuzer/index.html
The file was modified web/authors/kreuzer/index.xml
The file was modified web/authors/paulson/index.html
The file was modified web/authors/paulson/index.xml
The file was modified web/authors/sulejmani/index.html
The file was modified web/authors/sulejmani/index.xml
The file was modified web/data/keywords.json
The file was modified web/dependencies/bernoulli/index.html
The file was modified web/dependencies/bernoulli/index.xml
The file was modified web/dependencies/index.html
The file was modified web/dependencies/index.json
The file was modified web/dependencies/jacobson_basic_algebra/index.html
The file was modified web/dependencies/jacobson_basic_algebra/index.xml
The file was modified web/entries/BD_Security_Compositional.html
The file was modified web/entries/Bernoulli.html
The file was modified web/entries/Goedel_HFSet_Semantic.html
The file was modified web/entries/Goedel_Incompleteness.html
The file was modified web/entries/Hales_Jewett.html
The file was modified web/entries/Irrationals_From_THEBOOK.html
The file was modified web/entries/Jacobson_Basic_Algebra.html
The file was modified web/entries/Pluennecke_Ruzsa_Inequality.html
The file was modified web/entries/Residuated_Lattices.html
The file was modified web/entries/index.html
The file was modified web/entries/index.xml
The file was modified web/index.html
The file was modified web/index.json
The file was modified web/index.xml
The file was modified web/sitemap.xml
The file was modified web/statistics/index.html
The file was modified web/theories/index.xml
The file was modified web/topics/index.html
The file was modified web/topics/mathematics/combinatorics/index.html
The file was modified web/topics/mathematics/combinatorics/index.xml
Changeset 12981:c91e67482c60 by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry: Khovanski-Theorem
The file was addedthys/Khovanskii_Theorem/FiniteProduct.thy
The file was addedthys/Khovanskii_Theorem/For_2022.thy
The file was addedthys/Khovanskii_Theorem/Khovanskii.thy
The file was addedthys/Khovanskii_Theorem/ROOT
The file was addedthys/Khovanskii_Theorem/document/root.bib
The file was addedthys/Khovanskii_Theorem/document/root.tex
The file was modified thys/ROOTS
Changeset 12980:4b1af6f3fd24 by Manuel Eberl _manuel@pruvisto.org_:
fixed metadata for Hales_Jewett
The file was modified metadata/entries/Hales_Jewett.toml
Changeset 12979:7a3ce4a5cdf8 by Manuel Eberl _manuel@pruvisto.org_:
sitegen for Number_Theoretic_Transform
The file was addedmetadata/entries/Number_Theoretic_Transform.toml
The file was addedweb/entries/Number_Theoretic_Transform.html
The file was addedweb/theories/hales_jewett/index.html
The file was addedweb/theories/number_theoretic_transform/index.html
The file was modified metadata/authors.toml
The file was modified web/authors/ammer/index.html
The file was modified web/authors/ammer/index.xml
The file was modified web/authors/kreuzer/index.html
The file was modified web/authors/kreuzer/index.xml
The file was modified web/data/keywords.json
The file was modified web/dependencies/berlekamp_zassenhaus/index.html
The file was modified web/dependencies/berlekamp_zassenhaus/index.xml
The file was modified web/dependencies/index.html
The file was modified web/entries/Berlekamp_Zassenhaus.html
The file was modified web/entries/index.html
The file was modified web/entries/index.xml
The file was modified web/index.html
The file was modified web/index.json
The file was modified web/index.xml
The file was modified web/sitemap.xml
The file was modified web/statistics/index.html
The file was modified web/theories/index.xml
The file was modified web/topics/computer-science/algorithms/index.html
The file was modified web/topics/computer-science/algorithms/index.xml
The file was modified web/topics/computer-science/algorithms/mathematical/index.html
The file was modified web/topics/computer-science/algorithms/mathematical/index.xml
The file was modified web/topics/index.html
Changeset 12978:9480bd426471 by Manuel Eberl _manuel@pruvisto.org_:
new entry Number_Theoretic_Transform
The file was addedthys/Number_Theoretic_Transform/Butterfly.thy
The file was addedthys/Number_Theoretic_Transform/NTT.thy
The file was addedthys/Number_Theoretic_Transform/Preliminary_Lemmas.thy
The file was addedthys/Number_Theoretic_Transform/ROOT
The file was addedthys/Number_Theoretic_Transform/document/root.bib
The file was addedthys/Number_Theoretic_Transform/document/root.tex
The file was modified thys/ROOTS
Changeset 12977:a236359e9eb6 by nipkow:
new entry Hales Jewett
The file was addedmetadata/entries/Hales_Jewett.toml
The file was addedthys/Hales_Jewett/Hales_Jewett.thy
The file was addedthys/Hales_Jewett/ROOT
The file was addedthys/Hales_Jewett/document/root.bib
The file was addedthys/Hales_Jewett/document/root.tex
The file was addedweb/entries/Hales_Jewett.html
The file was modified metadata/authors.toml
The file was modified thys/ROOTS
The file was modified web/authors/eberl/index.html
The file was modified web/authors/eberl/index.xml
The file was modified web/authors/kreuzer/index.html
The file was modified web/authors/kreuzer/index.xml
The file was modified web/authors/sulejmani/index.html
The file was modified web/authors/sulejmani/index.xml
The file was modified web/data/keywords.json
The file was modified web/entries/BD_Security_Compositional.html
The file was modified web/entries/Goedel_HFSet_Semantic.html
The file was modified web/entries/Goedel_Incompleteness.html
The file was modified web/entries/Irrationals_From_THEBOOK.html
The file was modified web/entries/Residuated_Lattices.html
The file was modified web/entries/index.html
The file was modified web/entries/index.xml
The file was modified web/index.html
The file was modified web/index.json
The file was modified web/index.xml
The file was modified web/sitemap.xml
The file was modified web/statistics/index.html
The file was modified web/theories/index.xml
The file was modified web/topics/index.html
The file was modified web/topics/mathematics/combinatorics/index.html
The file was modified web/topics/mathematics/combinatorics/index.xml
Changeset 12976:17b82e6796f6 by fabian huch _huch@in.tum.de_:
adapt to only check ROOT for directories in thys (aftermath of Isabelle/a9bbf075f4319e920a22a1c0a5b763b6575f2089);
The file was modified tools/afp_check_roots.scala