Changes

Summary

Adapted QR Decomposition entry to the change of the GREATEST operator.
Adapted Hermite entry to the change of GREATEST.
Adapted Echelon Form entry to the change of GREATEST operator.
Changed GREATEST in order to use the one from the HOL Library, adapted the Gauss-Jordan entry.

Changeset 7976:c9fe0191ef4a by jodivaso: Adapted QR Decomposition entry to the change of the GREATEST operator.
The file was modified	`thys/QR_Decomposition/Gram_Schmidt.thy` (diff)
The file was modified	`thys/QR_Decomposition/QR_Efficient.thy` (diff)
Changeset 7975:2a8c91207478 by jodivaso: Adapted Hermite entry to the change of GREATEST.
The file was modified	`thys/Hermite/Hermite.thy` (diff)
Changeset 7974:40009cc269f5 by jodivaso: Adapted Echelon Form entry to the change of GREATEST operator.
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_IArrays.thy` (diff)
Changeset 7973:52f66f2a4f25 by jodivaso: Changed GREATEST in order to use the one from the HOL Library, adapted the Gauss-Jordan entry.
The file was modified	`thys/Gauss_Jordan/Bases_Of_Fundamental_Subspaces.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Bases_Of_Fundamental_Subspaces_IArrays.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Determinants2.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Gauss_Jordan.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Gauss_Jordan_PA.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Inverse.thy` (diff)
The file was modified	`thys/Gauss_Jordan/System_Of_Equations.thy` (diff)
The file was modified	`thys/Gauss_Jordan/System_Of_Equations_IArrays.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Dual_Order.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Mod_Type.thy` (diff)