Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned proof
  2. euclidean rings need no normalization
  3. prefer official global interface to remove code equations, leaving problematic situation due to bypassing of native code declarations as it is
  4. elementary definition of division on natural numbers
  5. removed unused lemmas
  6. tuned proofs
  7. avoid name clashes on interpretation of abstract locales
  8. abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
  9. Polynomial_Factorial does not depend on Field_as_Ring as such
  10. avoid unnecessary qualification
Changeset 8417:667ea8b4170e by haftmann:
tuned proof
The file was modified thys/Perron_Frobenius/Roots_Unity.thy (diff)
Changeset 8416:b63131b1652f by haftmann:
euclidean rings need no normalization
The file was modified thys/Berlekamp_Zassenhaus/Arithmetic_Record_Based.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Finite_Field.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Poly_Mod.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/ROOT (diff)
The file was modified thys/Berlekamp_Zassenhaus/Unique_Factorization_Poly.thy (diff)
The file was modified thys/Hermite/Hermite.thy (diff)
The file was modified thys/Matrix_Tensor/Matrix_Tensor.thy (diff)
The file was modified thys/Sqrt_Babylonian/NthRoot_Impl.thy (diff)
The file was modified thys/Stern_Brocot/Stern_Brocot_Tree.thy (diff)
The file was modified thys/Word_Lib/Word_Lemmas.thy (diff)
Changeset 8415:1e9b301624bf by haftmann:
prefer official global interface to remove code equations, leaving problematic situation due to bypassing of native code declarations as it is
The file was modified thys/Collections/ICF/tools/Record_Intf.thy (diff)
Changeset 8414:63ac715927ad by haftmann:
elementary definition of division on natural numbers
The file was modified thys/Affine_Arithmetic/Executable_Euclidean_Space.thy (diff)
The file was modified thys/Affine_Arithmetic/Floatarith_Expression.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy (diff)
The file was modified thys/Consensus_Refined/Consensus_Misc.thy (diff)
The file was modified thys/Consensus_Refined/Observing/BenOr_Proofs.thy (diff)
The file was modified thys/Consensus_Refined/Voting/OneThirdRule_Proofs.thy (diff)
The file was modified thys/Deep_Learning/DL_Deep_Model.thy (diff)
The file was modified thys/Deep_Learning/DL_Flatten_Matrix.thy (diff)
The file was modified thys/Deep_Learning/Tensor_Matricization.thy (diff)
The file was modified thys/Ergodic_Theory/Gouezel_Karlsson.thy (diff)
The file was modified thys/FocusStreamsCaseStudies/arith_hints.thy (diff)
The file was modified thys/Graph_Theory/Funpow.thy (diff)
The file was modified thys/Jordan_Hoelder/CompositionSeries.thy (diff)
The file was modified thys/List-Infinite/CommonArith/Util_Div.thy (diff)
The file was modified thys/LocalLexing/Ladder.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/Goodstein_Sequence.thy (diff)
The file was modified thys/Polynomial_Factorization/Prime_Factorization.thy (diff)
The file was modified thys/Polynomial_Interpolation/Improved_Code_Equations.thy (diff)
The file was modified thys/RSAPSS/Productdivides.thy (diff)
The file was modified thys/Recursion-Theory-I/PRecFun.thy (diff)
The file was modified thys/Refine_Imperative_HOL/IICF/Impl/IICF_Array_Matrix.thy (diff)
The file was modified thys/Refine_Imperative_HOL/IICF/Intf/IICF_Matrix.thy (diff)
The file was modified thys/Stable_Matching/Choice_Functions.thy (diff)
The file was modified thys/Stern_Brocot/Stern_Brocot_Tree.thy (diff)
The file was modified thys/Subresultants/Binary_Exponentiation.thy (diff)
The file was modified thys/Subresultants/Dichotomous_Lazard.thy (diff)
The file was modified thys/Word_Lib/Aligned.thy (diff)
The file was modified thys/Word_Lib/HOL_Lemmas.thy (diff)
The file was modified thys/Word_Lib/Word_Lemmas.thy (diff)
Changeset 8413:2a46d229991b by haftmann:
removed unused lemmas
The file was modified thys/Automatic_Refinement/Lib/Misc.thy (diff)
Changeset 8412:b84682d9ad58 by haftmann:
tuned proofs
The file was modified thys/Deep_Learning/DL_Missing_Sublist.thy (diff)
The file was modified thys/Euler_Partition/Euler_Partition.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/Goodstein_Sequence.thy (diff)
The file was modified thys/Promela/Promela.thy (diff)
The file was modified thys/Sturm_Tarski/PolyMisc.thy (diff)
The file was modified thys/Vickrey_Clarke_Groves/MiscTools.thy (diff)
Changeset 8411:c62af0c87bf7 by haftmann:
avoid name clashes on interpretation of abstract locales
The file was modified thys/Affine_Arithmetic/Executable_Euclidean_Space.thy (diff)
The file was modified thys/Algebraic_Numbers/Bivariate_Polynomials.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy (diff)
The file was modified thys/Bernoulli/Bernoulli_FPS.thy (diff)
The file was modified thys/Bertrands_Postulate/Bertrand.thy (diff)
The file was modified thys/Cauchy/CauchySchwarz.thy (diff)
The file was modified thys/Cayley_Hamilton/Square_Matrix.thy (diff)
The file was modified thys/Deep_Learning/DL_Network.thy (diff)
The file was modified thys/Deep_Learning/PP_Poly_Mapping.thy (diff)
The file was modified thys/Ergodic_Theory/SG_Library_Complement.thy (diff)
The file was modified thys/FFT/FFT.thy (diff)
The file was modified thys/First_Welfare_Theorem/Private_Ownership_Economy.thy (diff)
The file was modified thys/Gauss_Jordan/Linear_Maps.thy (diff)
The file was modified thys/Girth_Chromatic/Girth_Chromatic.thy (diff)
The file was modified thys/Jordan_Normal_Form/Matrix.thy (diff)
The file was modified thys/Jordan_Normal_Form/Matrix_Kernel.thy (diff)
The file was modified thys/Kleene_Algebra/Matrix.thy (diff)
The file was modified thys/List_Update/List_Factoring.thy (diff)
The file was modified thys/Markov_Models/Markov_Models_Auxiliary.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy (diff)
The file was modified thys/Perron_Frobenius/Perron_Frobenius_Aux_2.thy (diff)
The file was modified thys/Polynomial_Interpolation/Ring_Hom_Poly.thy (diff)
The file was modified thys/QR_Decomposition/Generalizations2.thy (diff)
The file was modified thys/Random_Graph_Subgraph_Threshold/Subgraph_Threshold.thy (diff)
The file was modified thys/Rep_Fin_Groups/Rep_Fin_Groups.thy (diff)
The file was modified thys/Stone_Relation_Algebras/Matrix_Relation_Algebras.thy (diff)
The file was modified thys/Tarskis_Geometry/Linear_Algebra2.thy (diff)
Changeset 8410:4cc52533cd91 by haftmann:
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
The file was modified thys/Akra_Bazzi/Eval_Numeral.thy (diff)
The file was modified thys/Automatic_Refinement/Lib/Misc.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Square_Free_Int_To_Square_Free_GFp.thy (diff)
The file was modified thys/Catalan_Numbers/Catalan_Numbers.thy (diff)
The file was modified thys/Deep_Learning/PP_MPoly.thy (diff)
The file was modified thys/Euler_Partition/Euler_Partition.thy (diff)
The file was modified thys/Hermite/Hermite.thy (diff)
The file was modified thys/Hermite/Hermite_IArrays.thy (diff)
The file was modified thys/Jordan_Normal_Form/Determinant.thy (diff)
The file was modified thys/List-Infinite/CommonArith/Util_Div.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/Multiset_More.thy (diff)
The file was modified thys/Polynomial_Factorization/Order_Polynomial.thy (diff)
The file was modified thys/Polynomial_Interpolation/Missing_Unsorted.thy (diff)
The file was modified thys/Polynomial_Interpolation/Ring_Hom_Poly.thy (diff)
The file was modified thys/Stern_Brocot/Stern_Brocot_Tree.thy (diff)
The file was modified thys/Vickrey_Clarke_Groves/UniformTieBreaking.thy (diff)
Changeset 8409:0c5977a8f8a2 by haftmann:
Polynomial_Factorial does not depend on Field_as_Ring as such
The file was modified thys/Berlekamp_Zassenhaus/Unique_Factorization_Poly.thy (diff)
The file was modified thys/Echelon_Form/Examples_Echelon_Form_Abstract.thy (diff)
The file was modified thys/Perron_Frobenius/Spectral_Radius_Theory.thy (diff)
The file was modified thys/Polynomial_Factorization/Gcd_Rat_Poly.thy (diff)
The file was modified thys/Rep_Fin_Groups/Rep_Fin_Groups.thy (diff)
The file was modified thys/Sturm_Sequences/Lib/Misc_Polynomial.thy (diff)
The file was modified thys/Sturm_Sequences/Sturm_Theorem.thy (diff)
The file was modified thys/Sturm_Tarski/Sturm_Tarski.thy (diff)
Changeset 8408:a61d9b28e2fb by haftmann:
avoid unnecessary qualification
The file was modified thys/Akra_Bazzi/Eval_Numeral.thy (diff)
The file was modified thys/Automatic_Refinement/Lib/Digraph_Basic.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Square_Free_Int_To_Square_Free_GFp.thy (diff)
The file was modified thys/CAVA_Automata/Lasso.thy (diff)
The file was modified thys/Echelon_Form/Echelon_Form.thy (diff)
The file was modified thys/Hermite/Hermite.thy (diff)
The file was modified thys/List-Infinite/CommonArith/Util_Div.thy (diff)
The file was modified thys/Native_Word/Native_Cast.thy (diff)
The file was modified thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Impl_Heapmap.thy (diff)
The file was modified thys/Vickrey_Clarke_Groves/UniformTieBreaking.thy (diff)