Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. merged
  2. added lemmas reflclp_(less|greater)_eq[simp], rtranclp_(less|greater)_eq[simp], and tranclp_(less|greater|less_eq|greater_eq)[simp]
  3. parallelize schedule optimization;
Changeset 79807:afb26a1dea71 by desharna:
merged
Changeset 79806:ba8fb71587ae by desharna:
added lemmas reflclp_(less|greater)_eq[simp], rtranclp_(less|greater)_eq[simp], and tranclp_(less|greater|less_eq|greater_eq)[simp]
The file was modified NEWS
The file was modified src/HOL/Library/Numeral_Type.thy
The file was modified src/HOL/Transitive_Closure.thy
Changeset 79805:45198ea3f0b3 by fabian huch _huch@in.tum.de_:
parallelize schedule optimization;
The file was modified src/Pure/Build/build_schedule.scala

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

Summary

  1. removed lemmas following Isabelle/ba8fb71587ae
  2. merge from AFP 2023
  3. sitegen for Wieferich Kempner
  4. new entry: Wieferich Kempner
  5. merge from AFP 2023
  6. metadata and sitegen for QBF-Solver
  7. new entry: QBF_Solver_Verification
  8. further files for CubicalCategories
  9. New entry CubicalCategories
  10. update doc;
  11. Correction of an error in the abstract
  12. sitegen for Karatsuba
  13. New submission: Karatsuba
  14. adjusted proof
Changeset 14106:289e12cecf5a by desharna:
removed lemmas following Isabelle/ba8fb71587ae
The file was modified thys/First_Order_Terms/Transitive_Closure_More.thy
The file was modified thys/Rank_Nullity_Theorem/Dual_Order.thy
Changeset 14105:5023c947e95e by rene thiemann _rene.thiemann@uibk.ac.at_:
merge from AFP 2023
Changeset 14104:53eb60336313 by rene thiemann _rene.thiemann@uibk.ac.at_:
sitegen for Wieferich Kempner
The file was addedmetadata/entries/Wieferich_Kempner.toml
The file was addedweb/authors/chenj/index.html
The file was addedweb/authors/chenj/index.xml
The file was addedweb/entries/Wieferich_Kempner.html
The file was addedweb/sessions/wieferich_kempner/index.html
The file was modified metadata/authors.toml
The file was modified metadata/authors.toml.orig
The file was modified web/authors/index.html
The file was modified web/authors/index.json
The file was modified web/data/keywords.json
The file was modified web/dependencies/index.html
The file was modified web/dependencies/three_squares/index.html
The file was modified web/dependencies/three_squares/index.xml
The file was modified web/entries/Polygonal_Number_Theorem.html
The file was modified web/entries/Three_Squares.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/sessions/index.xml
The file was modified web/sitemap.xml
The file was modified web/statistics/index.html
The file was modified web/topics/index.html
The file was modified web/topics/mathematics/index.xml
The file was modified web/topics/mathematics/number-theory/index.html
The file was modified web/topics/mathematics/number-theory/index.xml
Changeset 14103:5893fa2755ed by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry: Wieferich Kempner
The file was addedthys/Wieferich_Kempner/ROOT
The file was addedthys/Wieferich_Kempner/Wieferich_Kempner.thy
The file was addedthys/Wieferich_Kempner/document/root.bib
The file was addedthys/Wieferich_Kempner/document/root.tex
Changeset 14102:ab07e3da55f1 by rene thiemann _rene.thiemann@uibk.ac.at_:
merge from AFP 2023
Changeset 14101:95eee131bdb9 by rene thiemann _rene.thiemann@uibk.ac.at_:
metadata and sitegen for QBF-Solver
The file was addedmetadata/entries/QBF_Solver_Verification.toml
The file was addedweb/authors/bergstroem/index.html
The file was addedweb/authors/bergstroem/index.xml
The file was addedweb/entries/QBF_Solver_Verification.html
The file was addedweb/sessions/qbf_solver_verification/index.html
The file was modified metadata/authors.toml
The file was modified thys/ROOTS
The file was modified web/authors/index.html
The file was modified web/authors/index.json
The file was modified web/authors/weber/index.html
The file was modified web/authors/weber/index.xml
The file was modified web/data/keywords.json
The file was modified web/entries/Approximation_Algorithms.html
The file was modified web/entries/Catoids.html
The file was modified web/entries/Combinatorics_Words.html
The file was modified web/entries/CubicalCategories.html
The file was modified web/entries/Efficient_Weighted_Path_Order.html
The file was modified web/entries/Frequency_Moments.html
The file was modified web/entries/HoareForDivergence.html
The file was modified web/entries/HyperHoareLogic.html
The file was modified web/entries/Hypergraph_Colourings.html
The file was modified web/entries/List_Update.html
The file was modified web/entries/OmegaCatoidsQuantales.html
The file was modified web/entries/Polygonal_Number_Theorem.html
The file was modified web/entries/Prim_Dijkstra_Simple.html
The file was modified web/entries/Propositional_Proof_Systems.html
The file was modified web/entries/Quantales_Converse.html
The file was modified web/entries/S_Finite_Measure_Monad.html
The file was modified web/entries/Standard_Borel_Spaces.html
The file was modified web/entries/Transport.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/sessions/index.xml
The file was modified web/sitemap.xml
The file was modified web/statistics/index.html
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/index.xml
The file was modified web/topics/index.html
The file was modified web/topics/logic/general-logic/classical-propositional-logic/index.html
The file was modified web/topics/logic/general-logic/classical-propositional-logic/index.xml
The file was modified web/topics/logic/general-logic/index.xml
The file was modified web/topics/logic/index.xml
Changeset 14100:e2e483e2ef5f by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry: QBF_Solver_Verification
The file was addedthys/QBF_Solver_Verification/NaiveSolver.thy
The file was addedthys/QBF_Solver_Verification/PCNF.thy
The file was addedthys/QBF_Solver_Verification/Parser.thy
The file was addedthys/QBF_Solver_Verification/ROOT
The file was addedthys/QBF_Solver_Verification/SearchSolver.thy
The file was addedthys/QBF_Solver_Verification/SolverExport.thy
The file was addedthys/QBF_Solver_Verification/document/root.bib
The file was addedthys/QBF_Solver_Verification/document/root.tex
The file was modified thys/ROOTS
Changeset 14099:b13b8018f224 by nipkow:
further files for CubicalCategories
The file was addedmetadata/authors.toml.orig
The file was addedmetadata/entries/CubicalCategories.toml
The file was addedweb/authors/massacrier/index.html
The file was addedweb/authors/massacrier/index.xml
The file was addedweb/entries/CubicalCategories.html
The file was addedweb/sessions/cubicalcategories/index.html
Changeset 14098:de82d58c0e48 by nipkow:
New entry CubicalCategories
The file was addedthys/CubicalCategories/CubicalCategories.thy
The file was addedthys/CubicalCategories/CubicalCategoriesConnections.thy
The file was addedthys/CubicalCategories/CubicalOmegaZeroCategoriesConnections.thy
The file was addedthys/CubicalCategories/ICatoids.thy
The file was addedthys/CubicalCategories/ROOT
The file was addedthys/CubicalCategories/document/root.bib
The file was addedthys/CubicalCategories/document/root.tex
The file was modified metadata/authors.toml
The file was modified thys/ROOTS
The file was modified web/authors/index.html
The file was modified web/authors/index.json
The file was modified web/authors/struth/index.html
The file was modified web/authors/struth/index.xml
The file was modified web/data/keywords.json
The file was modified web/dependencies/catoids/index.html
The file was modified web/dependencies/catoids/index.xml
The file was modified web/entries/Approximation_Algorithms.html
The file was modified web/entries/Catoids.html
The file was modified web/entries/OmegaCatoidsQuantales.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/sessions/index.xml
The file was modified web/sitemap.xml
The file was modified web/statistics/index.html
The file was modified web/topics/index.html
The file was modified web/topics/mathematics/category-theory/index.html
The file was modified web/topics/mathematics/category-theory/index.xml
The file was modified web/topics/mathematics/index.xml
Changeset 14097:c724fc543bdf by fabian huch _huch@in.tum.de_:
update doc;
The file was modified doc/editors/new-entry-checkin.md
Changeset 14096:97de14bd03c6 by paulson _lp15@cam.ac.uk_:
Correction of an error in the abstract
The file was modified metadata/entries/Karatsuba.toml
The file was modified thys/Karatsuba/document/root.tex
The file was modified web/entries/Karatsuba.html
The file was modified web/index.json
Changeset 14095:41d96d664221 by paulson _lp15@cam.ac.uk_:
sitegen for Karatsuba
The file was addedmetadata/entries/Karatsuba.toml
The file was addedweb/authors/schulz/index.html
The file was addedweb/authors/schulz/index.xml
The file was addedweb/entries/Karatsuba.html
The file was addedweb/sessions/karatsuba/index.html
The file was modified metadata/authors.toml
The file was modified web/authors/index.html
The file was modified web/authors/index.json
The file was modified web/authors/karayel/index.html
The file was modified web/authors/karayel/index.xml
The file was modified web/data/keywords.json
The file was modified web/dependencies/akra_bazzi/index.html
The file was modified web/dependencies/akra_bazzi/index.xml
The file was modified web/dependencies/expander_graphs/index.html
The file was modified web/dependencies/expander_graphs/index.xml
The file was modified web/dependencies/index.html
The file was modified web/dependencies/root_balanced_tree/index.html
The file was modified web/dependencies/root_balanced_tree/index.xml
The file was modified web/entries/Akra_Bazzi.html
The file was modified web/entries/Catoids.html
The file was modified web/entries/Combinatorics_Words.html
The file was modified web/entries/Efficient_Weighted_Path_Order.html
The file was modified web/entries/Expander_Graphs.html
The file was modified web/entries/Frequency_Moments.html
The file was modified web/entries/HoareForDivergence.html
The file was modified web/entries/HyperHoareLogic.html
The file was modified web/entries/Hypergraph_Colourings.html
The file was modified web/entries/List_Update.html
The file was modified web/entries/OmegaCatoidsQuantales.html
The file was modified web/entries/Polygonal_Number_Theorem.html
The file was modified web/entries/Prim_Dijkstra_Simple.html
The file was modified web/entries/Propositional_Proof_Systems.html
The file was modified web/entries/Quantales_Converse.html
The file was modified web/entries/Root_Balanced_Tree.html
The file was modified web/entries/S_Finite_Measure_Monad.html
The file was modified web/entries/Standard_Borel_Spaces.html
The file was modified web/entries/Transport.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/sessions/index.xml
The file was modified web/sitemap.xml
The file was modified web/statistics/index.html
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/computer-science/index.xml
The file was modified web/topics/index.html
Changeset 14094:77c6d58a9e48 by paulson _lp15@cam.ac.uk_:
New submission: Karatsuba
The file was addedthys/Karatsuba/Binary_Representations/Abstract_Representations.thy
The file was addedthys/Karatsuba/Binary_Representations/Abstract_Representations_2.thy
The file was addedthys/Karatsuba/Binary_Representations/Int_LSBF.thy
The file was addedthys/Karatsuba/Binary_Representations/Nat_LSBF.thy
The file was addedthys/Karatsuba/Binary_Representations/Nat_LSBF_TM.thy
The file was addedthys/Karatsuba/Estimation_Method.thy
The file was addedthys/Karatsuba/Karatsuba/Karatsuba.thy
The file was addedthys/Karatsuba/Karatsuba/Karatsuba_Code_Nat.thy
The file was addedthys/Karatsuba/Karatsuba/Karatsuba_TM.thy
The file was addedthys/Karatsuba/Karatsuba_Runtime_Lemmas.thy
The file was addedthys/Karatsuba/Main_TM.thy
The file was addedthys/Karatsuba/Preliminaries/Karatsuba_Preliminaries.thy
The file was addedthys/Karatsuba/Preliminaries/Karatsuba_Sum_Lemmas.thy
The file was addedthys/Karatsuba/Preliminaries/Monoid_Sums.thy
The file was addedthys/Karatsuba/ROOT
The file was addedthys/Karatsuba/Time_Monad_Extended.thy
The file was addedthys/Karatsuba/document/root.bib
The file was addedthys/Karatsuba/document/root.tex
The file was modified thys/ROOTS
Changeset 14093:a87e290b359d by rene thiemann _rene.thiemann@uibk.ac.at_:
adjusted proof
The file was modified thys/LLL_Basis_Reduction/Missing_Lemmas.thy