Changes

Summary

moved lemmas, and moved Missing_Unsorted from JNF to P-Interpolation
added algorithm for binary exponentiation (or exponentiation by squaring)

Changeset 6195:82c3559552a3 by rene thiemann _rene.thiemann@uibk.ac.at_: moved lemmas, and moved Missing_Unsorted from JNF to P-Interpolation
The file was added	`thys/Polynomial_Interpolation/Missing_Unsorted.thy`
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Compare_Complex.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/ROOT` (diff)
The file was modified	`thys/Algebraic_Numbers/Unique_Factorization_Poly.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/document/root.tex` (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/Jordan_Normal_Form.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/ROOT` (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/ROOT` (diff)
The file was modified	`thys/Polynomial_Factorization/Unique_Factorization_Domain.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Polynomial.thy` (diff)
The file was removed	`thys/Jordan_Normal_Form/Missing_Unsorted.thy`
Changeset 6194:6e06ef266d51 by rene thiemann _rene.thiemann@uibk.ac.at_: added algorithm for binary exponentiation (or exponentiation by squaring)
The file was added	`thys/Algebraic_Numbers/Binary_Exponentiation.thy`
The file was modified	`thys/Algebraic_Numbers/Resultant.thy` (diff)