Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. renamed thms to avoid name clashes
  2. fix document preparation
  3. update metadata
  4. more readable constructors for multivariate polynomials
  5. updates by Alexander Maletzky: restructured dgrad_p_set dgrad_p_set_le; split theories Reduction and Buchberger_Algorithm off Groebner_Bases
  6. more updates and generalizations by Alexander Maletzky: prefer gd_powerprod, added criteria to improve efficiency of gbaux
  7. renaming and moving theories about polynomials
  8. type fmap for implementation of type poly_mapping
  9. updates and generalizations by Alexander Maletzky
  10. perspective projection
Changeset 8819:3aa31cbe90aa by immler:
renamed thms to avoid name clashes
The file was modified thys/Containers/RBT_Set2.thy (diff)
The file was modified thys/Containers/RBT_ext.thy (diff)
The file was modified thys/Containers/Set_Linorder.thy (diff)
Changeset 8818:685b2c4d18f7 by immler:
fix document preparation
The file was modified thys/Groebner_Bases/Buchberger_Algorithm.thy (diff)
The file was modified thys/Groebner_Bases/Groebner_Bases.thy (diff)
The file was modified thys/Groebner_Bases/document/root.tex (diff)
The file was modified thys/Polynomials/MPoly_Type_Class.thy (diff)
The file was modified thys/Polynomials/Power_Products.thy (diff)
The file was modified thys/Polynomials/document/root.tex (diff)
Changeset 8817:6a7b63268058 by immler:
update metadata
The file was modified metadata/metadata (diff)
The file was modified thys/Polynomials/Poly_Mapping_Finite_Map.thy (diff)
Changeset 8816:a1a771ef0713 by immler:
more readable constructors for multivariate polynomials
The file was modified thys/Groebner_Bases/Computations.thy (diff)
The file was modified thys/Polynomials/MPoly_Type.thy (diff)
The file was modified thys/Polynomials/MPoly_Type_Class_FMap.thy (diff)
The file was modified thys/Polynomials/Poly_Mapping.thy (diff)
The file was modified thys/Polynomials/Poly_Mapping_Finite_Map.thy (diff)
Changeset 8815:d171a315f877 by immler:
updates by Alexander Maletzky: restructured dgrad_p_set dgrad_p_set_le; split theories Reduction and Buchberger_Algorithm off Groebner_Bases
The file was addedthys/Groebner_Bases/Buchberger_Algorithm.thy
The file was addedthys/Groebner_Bases/Reduction.thy
The file was modified thys/Groebner_Bases/Computations.thy (diff)
The file was modified thys/Groebner_Bases/General.thy (diff)
The file was modified thys/Groebner_Bases/Groebner_Bases.thy (diff)
The file was modified thys/Polynomials/MPoly_Type_Class.thy (diff)
The file was modified thys/Polynomials/MPoly_Type_Class_FMap.thy (diff)
The file was modified thys/Polynomials/Poly_Mapping.thy (diff)
The file was modified thys/Polynomials/Power_Products.thy (diff)
Changeset 8814:393402f14f02 by immler:
more updates and generalizations by Alexander Maletzky: prefer gd_powerprod, added criteria to improve efficiency of gbaux
The file was addedthys/Groebner_Bases/General.thy
The file was modified thys/Groebner_Bases/Computations.thy (diff)
The file was modified thys/Groebner_Bases/Confluence.thy (diff)
The file was modified thys/Groebner_Bases/Groebner_Bases.thy (diff)
The file was modified thys/Polynomials/MPoly_Type_Class.thy (diff)
The file was modified thys/Polynomials/MPoly_Type_Class_FMap.thy (diff)
The file was modified thys/Polynomials/Poly_Mapping.thy (diff)
The file was modified thys/Polynomials/Power_Products.thy (diff)
Changeset 8813:5e8ecabee58b by immler:
renaming and moving theories about polynomials
The file was addedthys/Polynomials/MPoly_Type.thy
The file was addedthys/Polynomials/MPoly_Type_Class.thy
The file was addedthys/Polynomials/MPoly_Type_Class_FMap.thy
The file was addedthys/Polynomials/MPoly_Type_Univariate.thy
The file was addedthys/Polynomials/More_List2.thy
The file was addedthys/Polynomials/More_MPoly_Type.thy
The file was addedthys/Polynomials/Poly_Mapping.thy
The file was modified thys/Deep_Learning/DL_Deep_Model_Poly.thy (diff)
The file was modified thys/Deep_Learning/Lebesgue_Zero_Set.thy (diff)
The file was modified thys/Deep_Learning/ROOT (diff)
The file was modified thys/Groebner_Bases/Computations.thy (diff)
The file was modified thys/Groebner_Bases/Groebner_Bases.thy (diff)
The file was modified thys/Groebner_Bases/ROOT (diff)
The file was modified thys/Polynomials/Poly_Mapping_Finite_Map.thy (diff)
The file was modified thys/Polynomials/Power_Products.thy (diff)
The file was modified thys/Polynomials/ROOT (diff)
The file was removedthys/Deep_Learning/PP_MPoly.thy
The file was removedthys/Deep_Learning/PP_More_List2.thy
The file was removedthys/Deep_Learning/PP_More_MPoly.thy
The file was removedthys/Deep_Learning/PP_Poly_Mapping.thy
The file was removedthys/Deep_Learning/PP_Univariate.thy
The file was removedthys/Polynomials/Abstract_Poly.thy
The file was removedthys/Polynomials/Poly_Lists.thy
Changeset 8812:370db8240e5a by immler:
type fmap for implementation of type poly_mapping
The file was addedthys/Polynomials/Poly_Mapping_Finite_Map.thy
The file was modified thys/Deep_Learning/PP_Poly_Mapping.thy (diff)
The file was modified thys/Groebner_Bases/Computations.thy (diff)
The file was modified thys/Polynomials/Abstract_Poly.thy (diff)
The file was modified thys/Polynomials/Poly_Lists.thy (diff)
The file was modified thys/Polynomials/Power_Products.thy (diff)
Changeset 8811:cbdce7e3cdb4 by immler:
updates and generalizations by Alexander Maletzky
The file was modified thys/Groebner_Bases/Computations.thy (diff)
The file was modified thys/Groebner_Bases/Groebner_Bases.thy (diff)
The file was modified thys/Groebner_Bases/ROOT (diff)
The file was modified thys/Polynomials/Abstract_Poly.thy (diff)
The file was modified thys/Polynomials/Poly_Lists.thy (diff)
The file was modified thys/Polynomials/Power_Products.thy (diff)
The file was modified thys/Polynomials/ROOT (diff)
Changeset 8810:f48f07a88e66 by immler:
perspective projection
The file was modified thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy (diff)