src/HOL/Matrix/Matrix.thy
changeset 17919 09adb77ac16c
parent 17915 e38947f9ba5e
child 20633 e98f59806244
equal deleted inserted replaced
17918:93e26302733e 17919:09adb77ac16c