src/HOL/RealVector.thy
changeset 36473 8a5c99a1c965
parent 36409 d323e7773aa8
child 36795 e05e1283c550
equal deleted inserted replaced
36422:69004340f53c 36473:8a5c99a1c965