Summary
- use non-recursive definition of eliminate entries
The file was modified | thys/Jordan_Normal_Form/Gauss_Jordan_Elimination.thy (diff) |
The file was modified | thys/Jordan_Normal_Form/Gauss_Jordan_IArray_Impl.thy (diff) |
The file was modified | thys/Polynomial_Factorization/Gauss_Jordan_Field.thy (diff) |