src/HOL/RealVector.thy
changeset 30151 629f3a92863e
parent 30070 76cee7c62782
child 30242 aea5d7fa7ef5
equal deleted inserted replaced
30150:4d5a98cebb24 30151:629f3a92863e