Summary
- separate type class for arbitrary quotient and remainder partitions; [cont] > stripped dependency on pragmatic type class semiring_div as far as possible
The file was modified | thys/Echelon_Form/Echelon_Form_Inverse.thy (diff) |
The file was modified | thys/Echelon_Form/Rings2.thy (diff) |
The file was modified | thys/Hermite/Hermite.thy (diff) |
The file was modified | thys/JinjaThreads/Common/BinOp.thy (diff) |
The file was modified | thys/Matrix_Tensor/Matrix_Tensor.thy (diff) |
The file was modified | thys/Native_Word/Word_Misc.thy (diff) |