Changes

Summary

adapted Perron-Frobenius from submission to development-version, merged and moved lemmas to correct places
merge Square_Free_Factorization and Square_Free_Factorization_Patched
started to adjust to devel version

Changeset 6634:7a770b29baaa by rene thiemann _rene.thiemann@uibk.ac.at_: adapted Perron-Frobenius from submission to development-version, merged and moved lemmas to correct places
The file was modified	`thys/Jordan_Normal_Form/Char_Poly.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix.thy` (diff)
The file was modified	`thys/Perron_Frobenius/HMA_Connect.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/ROOT` (diff)
The file was modified	`thys/Perron_Frobenius/Spectral_Radius_Theory.thy` (diff)
The file was removed	`thys/Perron_Frobenius/Eigenvector_Homomorphism.thy`
Changeset 6633:47f3b3781a7e by rene thiemann _rene.thiemann@uibk.ac.at_: merge Square_Free_Factorization and Square_Free_Factorization_Patched
The file was modified	`thys/Algebraic_Numbers/Sturm_Rat.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/Ring_Hom.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom_Poly.thy` (diff)
The file was removed	`thys/Perron_Frobenius/Square_Free_Factorization_Patched.thy`
Changeset 6632:4271a8c5a8f8 by nipkow: started to adjust to devel version
The file was modified	`thys/Perron_Frobenius/Perron_Frobenius.thy` (diff)