Summary
- merge
- moved g_bound into partial invariant of LLL_algorithm, changed order of parameters for dk
- fixes for MIN, MAX and *s = *r
The file was modified | thys/LLL_Basis_Reduction/LLL.thy (diff) |
The file was modified | thys/Affine_Arithmetic/Counterclockwise.thy (diff) |
The file was modified | thys/Architectural_Design_Patterns/Blockchain.thy (diff) |
The file was modified | thys/Cayley_Hamilton/Square_Matrix.thy (diff) |
The file was modified | thys/Jordan_Normal_Form/Jordan_Normal_Form_Existence.thy (diff) |
The file was modified | thys/Perron_Frobenius/Perron_Frobenius_Irreducible.thy (diff) |
The file was modified | thys/QR_Decomposition/Miscellaneous_QR.thy (diff) |
The file was modified | thys/Tarskis_Geometry/Linear_Algebra2.thy (diff) |