Summary
- more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
The file was modified | thys/Fermat3_4/QuadForm.thy (diff) |
The file was modified | thys/Jordan_Normal_Form/Determinant.thy (diff) |
The file was modified | thys/Fermat3_4/QuadForm.thy (diff) |
The file was modified | thys/Jordan_Normal_Form/Determinant.thy (diff) |