src/HOL/Real_Vector_Spaces.thy
changeset 57362 3ae07451a9f5
parent 57276 49c51eeaa623
child 57418 6ab1c7cb0b8d
equal deleted inserted replaced
57361:05fda107fb89 57362:3ae07451a9f5