Changes

Summary

Changeset 9245:09661d78e6db by rene thiemann _rene.thiemann@uibk.ac.at_: cleanup in Gram-Schmidt_2: less dependence on gram_schmidt, use gso instead
The file was modified	`thys/Jordan_Normal_Form/Gram_Schmidt.thy` (diff)
The file was modified	`thys/LLL_Basis_Reduction/Gram_Schmidt_2.thy` (diff)
The file was modified	`thys/LLL_Basis_Reduction/LLL.thy` (diff)
The file was modified	`thys/LLL_Basis_Reduction/LLL_Complexity.thy` (diff)
The file was modified	`thys/LLL_Basis_Reduction/LLL_GSO_Impl.thy` (diff)
The file was modified	`thys/LLL_Basis_Reduction/LLL_Integer_Equations.thy` (diff)
The file was modified	`thys/LLL_Basis_Reduction/LLL_Mu_Impl.thy` (diff)
The file was modified	`thys/LLL_Basis_Reduction/LLL_Mu_Integer_Impl.thy` (diff)
The file was modified	`thys/LLL_Basis_Reduction/LLL_Number_Bounds.thy` (diff)