Changes

Summary

def -> define

Changeset 7251:35389a723a56 by rene thiemann _rene.thiemann@uibk.ac.at_: def -> define
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Resultant.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/Determinant_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gauss_Jordan_Elimination.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gauss_Jordan_IArray_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gram_Schmidt.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form_Existence.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form_Uniqueness.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Comparison.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Complexity.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Kernel.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Missing_Permutations.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Missing_VectorSpace.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Schur_Decomposition.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Spectral_Radius.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/VS_Connect.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Bij_Nat.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Cancel_Card_Constraint.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Perron_Frobenius.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Perron_Frobenius_Aux.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Spectral_Radius_Theory.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Dvd_Int_Poly.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Explicit_Roots.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Fundamental_Theorem_Algebra_Factorized.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Gauss_Lemma.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Kronecker_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Order_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Polynomial_Division.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Rational_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Rational_Root_Test.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Square_Free_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Is_Rat_To_Rat.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/Neville_Aitken_Interpolation.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Newton_Interpolation.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Polynomial_Interpolation.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom_Poly.thy` (diff)