Skip to content
Failed

Changes

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

Summary

  1. move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations into Algebraic_Numbers
  2. ported Cubic_Quartic_Equations from AFP 2021 to devel
  3. merge of AFP 2021
  4. Cubic_Quartic_Equations sitegen
  5. new entry Cubic_Quartic_Equations
  6. sitegen for combinatorial design theory
  7. new entry: Combinatorial Design Theory
  8. sitegen for Three Circles
  9. new entry: Three Circles
Changeset 12025:fbfac64da6d5 by rene thiemann _rene.thiemann@uibk.ac.at_:
move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations into Algebraic_Numbers
The file was addedthys/Algebraic_Numbers/Min_Int_Poly.thy
The file was addedthys/Cubic_Quartic_Equations/Min_Int_Poly_Complex_Impl.thy
The file was addedthys/Hermite_Lindemann/More_Min_Int_Poly.thy
The file was modified thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy
The file was modified thys/Cubic_Quartic_Equations/Complex_Roots.thy
The file was modified thys/Cubic_Quartic_Equations/Cubic_Polynomials.thy
The file was modified thys/Cubic_Quartic_Equations/Quartic_Polynomials.thy
The file was modified thys/Cubic_Quartic_Equations/ROOT
The file was modified thys/Hermite_Lindemann/Hermite_Lindemann.thy
The file was modified thys/Polynomial_Factorization/Explicit_Roots.thy
The file was removedthys/Cubic_Quartic_Equations/Min_Int_Poly_Impl.thy
The file was removedthys/Hermite_Lindemann/Min_Int_Poly.thy
Changeset 12024:6929ff388470 by rene thiemann _rene.thiemann@uibk.ac.at_:
ported Cubic_Quartic_Equations from AFP 2021 to devel
The file was modified thys/Cubic_Quartic_Equations/Complex_Roots.thy
Changeset 12022:7e6431c07123 by paulson _lp15@cam.ac.uk_:
Cubic_Quartic_Equations sitegen
The file was addedweb/entries/Cubic_Quartic_Equations.html
The file was modified metadata/metadata
The file was modified web/entries/Algebraic_Numbers.html
The file was modified web/entries/Complex_Geometry.html
The file was modified web/entries/Hermite_Lindemann.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 12021:c4a4c0f9e4c8 by paulson _lp15@cam.ac.uk_:
new entry Cubic_Quartic_Equations
The file was addedthys/Cubic_Quartic_Equations/Cardanos_Formula.thy
The file was addedthys/Cubic_Quartic_Equations/Complex_Roots.thy
The file was addedthys/Cubic_Quartic_Equations/Cubic_Polynomials.thy
The file was addedthys/Cubic_Quartic_Equations/Ferraris_Formula.thy
The file was addedthys/Cubic_Quartic_Equations/Min_Int_Poly_Impl.thy
The file was addedthys/Cubic_Quartic_Equations/Quartic_Polynomials.thy
The file was addedthys/Cubic_Quartic_Equations/ROOT
The file was addedthys/Cubic_Quartic_Equations/document/root.bib
The file was addedthys/Cubic_Quartic_Equations/document/root.tex
The file was modified thys/ROOTS
Changeset 12020:56c3e661569f by rene thiemann _rene.thiemann@uibk.ac.at_:
sitegen for combinatorial design theory
The file was addedweb/entries/Design_Theory.html
The file was modified metadata/metadata
The file was modified web/entries/Card_Partitions.html
The file was modified web/entries/Graph_Theory.html
The file was modified web/entries/Lucas_Theorem.html
The file was modified web/entries/Nested_Multisets_Ordinals.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 12019:7654a7c1d7af by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry: Combinatorial Design Theory
The file was addedthys/Design_Theory/BIBD.thy
The file was addedthys/Design_Theory/Block_Designs.thy
The file was addedthys/Design_Theory/Design_Basics.thy
The file was addedthys/Design_Theory/Design_Isomorphisms.thy
The file was addedthys/Design_Theory/Design_Operations.thy
The file was addedthys/Design_Theory/Design_Theory_Root.thy
The file was addedthys/Design_Theory/Designs_And_Graphs.thy
The file was addedthys/Design_Theory/Group_Divisible_Designs.thy
The file was addedthys/Design_Theory/Multisets_Extras.thy
The file was addedthys/Design_Theory/ROOT
The file was addedthys/Design_Theory/Resolvable_Designs.thy
The file was addedthys/Design_Theory/Sub_Designs.thy
The file was addedthys/Design_Theory/document/root.bib
The file was addedthys/Design_Theory/document/root.tex
The file was modified thys/ROOTS
Changeset 12018:65f00954b8a3 by rene thiemann _rene.thiemann@uibk.ac.at_:
sitegen for Three Circles
The file was addedweb/entries/Three_Circles.html
The file was modified metadata/metadata
The file was modified web/entries/Budan_Fourier.html
The file was modified web/entries/Polynomial_Interpolation.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 12017:41bc6e38e99f by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry: Three Circles
The file was addedthys/Three_Circles/Bernstein.thy
The file was addedthys/Three_Circles/Bernstein_01.thy
The file was addedthys/Three_Circles/Normal_Poly.thy
The file was addedthys/Three_Circles/ROOT
The file was addedthys/Three_Circles/RRI_Misc.thy
The file was addedthys/Three_Circles/Three_Circles.thy
The file was addedthys/Three_Circles/document/root.bib
The file was addedthys/Three_Circles/document/root.tex
The file was modified thys/ROOTS