Skip to content
[Jenkins]Jenkins
log in
Success

Changes

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

Summary

  1. merged
  2. clarified signature: more operations;
  3. tuned signature;
  4. tuned, following hints by IntelliJ IDEA;
  5. clarified signature, to support external tools like "isabelle narration";
  6. syntactic type classes for signed division operators
  7. reduce prominence of facts
Changeset 76237:0a44395a25f0 by wenzelm:
merged
Changeset 76236:03dd2f19f1d7 by wenzelm:
clarified signature: more operations;
The file was modified src/Pure/General/bytes.scala
Changeset 76235:16c12979c132 by wenzelm:
tuned signature;
The file was modified src/Pure/General/symbol.scala
The file was modified src/Pure/PIDE/document.scala
The file was modified src/Pure/PIDE/text.scala
Changeset 76234:035ffcd82fb2 by wenzelm:
tuned, following hints by IntelliJ IDEA;
The file was modified src/Pure/PIDE/command.scala
Changeset 76233:f3b23f4eaaac by wenzelm:
clarified signature, to support external tools like "isabelle narration";
The file was modified src/Pure/PIDE/rendering.scala
Changeset 76232:a7ccb744047b by haftmann:
syntactic type classes for signed division operators
The file was modified src/HOL/Library/Signed_Division.thy
Changeset 76231:8a48e18f081e by haftmann:
reduce prominence of facts
The file was modified src/HOL/Divides.thy
The file was modified src/HOL/Euclidean_Division.thy
The file was modified src/HOL/Library/Numeral_Type.thy
The file was modified src/HOL/Library/Omega_Words_Fun.thy
The file was modified src/HOL/Library/Word.thy
The file was modified src/HOL/Number_Theory/Cong.thy
The file was modified src/HOL/Number_Theory/Pocklington.thy
The file was modified src/HOL/UNITY/Simple/Token.thy

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

Summary

  1. tuned proofs
  2. merge from afp-2021-1
  3. new entry Undirected_Graph_Theory
  4. typo
  5. typo
  6. New entry: Maximum_Segment_Sum
  7. regenerate site;
  8. added topic for data management systems;
  9. added missing file
  10. New entry Safe_Range_RC
Changeset 13067:a74db29363f5 by haftmann:
tuned proofs
The file was modified thys/Affine_Arithmetic/Executable_Euclidean_Space.thy
The file was modified thys/BenOr_Kozen_Reif/BKR_Proofs.thy
The file was modified thys/Berlekamp_Zassenhaus/Poly_Mod_Finite_Field_Record_Based.thy
The file was modified thys/CRYSTALS-Kyber/Abs_Qr.thy
The file was modified thys/Case_Labeling/Examples/Monadic_Language.thy
The file was modified thys/Consensus_Refined/Consensus_Misc.thy
The file was modified thys/Digit_Expansions/Carries.thy
The file was modified thys/Diophantine_Eqns_Lin_Hom/Linear_Diophantine_Equations.thy
The file was modified thys/Dirichlet_L/Dirichlet_Characters.thy
The file was modified thys/Gauss_Sums/Gauss_Sums.thy
The file was modified thys/Group-Ring-Module/Algebra4.thy
The file was modified thys/List-Infinite/CommonArith/Util_Div.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy
The file was modified thys/Padic_Field/Padic_Field_Powers.thy
The file was modified thys/Probabilistic_Prime_Tests/Jacobi_Symbol.thy
The file was modified thys/Rank_Nullity_Theorem/Mod_Type.thy
The file was modified thys/SumSquares/FourSquares.thy
The file was modified thys/Valuation/Valuation1.thy
The file was modified thys/Virtual_Substitution/OptimizationProofs.thy
The file was modified thys/Word_Lib/Bits_Int.thy
The file was modified thys/Word_Lib/Reversed_Bit_Lists.thy
Changeset 13066:6100f6dbbfed by gerwin klein _kleing@unsw.edu.au_:
merge from afp-2021-1
Changeset 13065:2482f4650245 by gerwin klein _kleing@unsw.edu.au_:
new entry Undirected_Graph_Theory
The file was addedmetadata/entries/Undirected_Graph_Theory.toml
The file was addedthys/Undirected_Graph_Theory/Bipartite_Graphs.thy
The file was addedthys/Undirected_Graph_Theory/Connectivity.thy
The file was addedthys/Undirected_Graph_Theory/Girth_Independence.thy
The file was addedthys/Undirected_Graph_Theory/Graph_Theory_Relations.thy
The file was addedthys/Undirected_Graph_Theory/Graph_Triangles.thy
The file was addedthys/Undirected_Graph_Theory/ROOT
The file was addedthys/Undirected_Graph_Theory/Undirected_Graph_Basics.thy
The file was addedthys/Undirected_Graph_Theory/Undirected_Graph_Walks.thy
The file was addedthys/Undirected_Graph_Theory/Undirected_Graphs_Root.thy
The file was addedthys/Undirected_Graph_Theory/document/root.bib
The file was addedthys/Undirected_Graph_Theory/document/root.log
The file was addedthys/Undirected_Graph_Theory/document/root.tex
The file was addedweb/entries/Undirected_Graph_Theory.html
The file was addedweb/theories/undirected_graph_theory/index.html
The file was modified thys/ROOTS
The file was modified web/authors/edmonds/index.html
The file was modified web/authors/edmonds/index.xml
The file was modified web/data/keywords.json
The file was modified web/dependencies/design_theory/index.html
The file was modified web/dependencies/design_theory/index.xml
The file was modified web/dependencies/girth_chromatic/index.html
The file was modified web/dependencies/girth_chromatic/index.xml
The file was modified web/dependencies/index.html
The file was modified web/entries/Design_Theory.html
The file was modified web/entries/Girth_Chromatic.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/graph-theory/index.html
The file was modified web/topics/mathematics/graph-theory/index.xml
Changeset 13064:21836ba5b3e6 by nipkow:
typo
The file was modified web/authors/cremer/index.html
The file was modified web/authors/cremer/index.xml
The file was modified web/entries/Equivalence_Relation_Enumeration.html
The file was modified web/entries/Maximum_Segment_Sum.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/topics/computer-science/algorithms/index.html
The file was modified web/topics/computer-science/algorithms/index.xml
Changeset 13063:8dd014d07166 by nipkow:
typo
The file was modified metadata/entries/Maximum_Segment_Sum.toml
Changeset 13062:a791f4f48a75 by nipkow:
New entry: Maximum_Segment_Sum
The file was addedmetadata/entries/Maximum_Segment_Sum.toml
The file was addedthys/Maximum_Segment_Sum/Maximum_Segment_Sum.thy
The file was addedthys/Maximum_Segment_Sum/ROOT
The file was addedthys/Maximum_Segment_Sum/document/root.bib
The file was addedthys/Maximum_Segment_Sum/document/root.tex
The file was addedweb/authors/cremer/index.html
The file was addedweb/authors/cremer/index.xml
The file was addedweb/entries/Maximum_Segment_Sum.html
The file was addedweb/theories/maximum_segment_sum/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/data/keywords.json
The file was modified web/entries/Equivalence_Relation_Enumeration.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/index.html
Changeset 13061:549a8c591678 by fabian huch _huch@in.tum.de_:
regenerate site;
The file was addedweb/topics/computer-science/data-management-systems/index.html
The file was addedweb/topics/computer-science/data-management-systems/index.xml
The file was modified web/entries/BTree.html
The file was modified web/entries/Eval_FO.html
The file was modified web/entries/Generic_Join.html
The file was modified web/entries/Safe_Range_RC.html
The file was modified web/index.json
The file was modified web/sitemap.xml
The file was modified web/topics/index.html
The file was modified web/topics/index.json
Changeset 13060:811ba4df645d by fabian huch _huch@in.tum.de_:
added topic for data management systems;
The file was modified metadata/entries/BTree.toml
The file was modified metadata/entries/Eval_FO.toml
The file was modified metadata/entries/Generic_Join.toml
The file was modified metadata/entries/Safe_Range_RC.toml
The file was modified metadata/topics.toml
Changeset 13059:25d277910e1a by nipkow:
added missing file
The file was addedweb/theories/safe_range_rc/index.html
Changeset 13058:d4348f7b41ae by nipkow:
New entry Safe_Range_RC
The file was addedmetadata/entries/Safe_Range_RC.toml
The file was addedthys/Safe_Range_RC/Examples.thy
The file was addedthys/Safe_Range_RC/Preliminaries.thy
The file was addedthys/Safe_Range_RC/ROOT
The file was addedthys/Safe_Range_RC/Relational_Calculus.thy
The file was addedthys/Safe_Range_RC/Restrict_Bounds.thy
The file was addedthys/Safe_Range_RC/Restrict_Bounds_Impl.thy
The file was addedthys/Safe_Range_RC/Restrict_Frees.thy
The file was addedthys/Safe_Range_RC/Restrict_Frees_Impl.thy
The file was addedthys/Safe_Range_RC/Results.thy
The file was addedthys/Safe_Range_RC/document/root.bib
The file was addedthys/Safe_Range_RC/document/root.tex
The file was addedweb/entries/Safe_Range_RC.html
The file was modified thys/ROOTS
The file was modified web/authors/raszyk/index.html
The file was modified web/authors/raszyk/index.xml
The file was modified web/authors/traytel/index.html
The file was modified web/authors/traytel/index.xml
The file was modified web/data/keywords.json
The file was modified web/dependencies/collections/index.html
The file was modified web/dependencies/collections/index.xml
The file was modified web/dependencies/deriving/index.html
The file was modified web/dependencies/deriving/index.xml
The file was modified web/dependencies/index.html
The file was modified web/dependencies/list-index/index.html
The file was modified web/dependencies/list-index/index.xml
The file was modified web/entries/Collections.html
The file was modified web/entries/Deriving.html
The file was modified web/entries/List-Index.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/logic/general-logic/classical-first-order-logic/index.html
The file was modified web/topics/logic/general-logic/classical-first-order-logic/index.xml
The file was modified web/topics/logic/general-logic/index.html
The file was modified web/topics/logic/general-logic/index.xml