Changes

Summary

setprod -> prod

Changeset 7211:ea6696815b2d by nipkow: setprod -> prod
The file was modified	`thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Complex_Roots_Real_Poly.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Roots.thy` (diff)
The file was modified	`thys/Bell_Numbers_Spivey/Bell_Numbers.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/Factorize_Int_Poly.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Factorize_Rat_Poly.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy` (diff)
The file was modified	`thys/Cayley_Hamilton/Cayley_Hamilton.thy` (diff)
The file was modified	`thys/Cayley_Hamilton/Square_Matrix.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_Det.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_Det_IArrays.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Determinants2.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Determinants_IArrays.thy` (diff)
The file was modified	`thys/Group-Ring-Module/Algebra3.thy` (diff)
The file was modified	`thys/Hermite/Hermite.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Char_Poly.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Determinant.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_IArray_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Missing_Permutations.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/VS_Connect.thy` (diff)
The file was modified	`thys/Markov_Models/Continuous_Time_Markov_Chain.thy` (diff)
The file was modified	`thys/Markov_Models/Trace_Space_Equals_Markov_Processes.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Gossip_Broadcast.thy` (diff)
The file was modified	`thys/Perron_Frobenius/HMA_Connect.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Polynomial_Divisibility.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Prime_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Rational_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Square_Free_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Unsorted.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom.thy` (diff)
The file was modified	`thys/Prime_Harmonic_Series/Prime_Harmonic.thy` (diff)
The file was modified	`thys/Prime_Harmonic_Series/Prime_Harmonic_Misc.thy` (diff)
The file was modified	`thys/Prime_Harmonic_Series/Squarefree_Nat.thy` (diff)
The file was modified	`thys/QR_Decomposition/QR_Decomposition.thy` (diff)
The file was modified	`thys/Random_Graph_Subgraph_Threshold/Ugraph_Misc.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Generalizations.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/NthRoot_Impl.thy` (diff)
The file was modified	`thys/Stirling_Formula/Stirling_Formula.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Triangular_Function.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Up_Down.thy` (diff)