src/HOL/RealVector.thy
changeset 36258 f459a0cc3241
parent 35216 7641e8d831d2
child 36349 39be26d1bc28
equal deleted inserted replaced
36257:3f3e9f18f302 36258:f459a0cc3241