src/HOL/Real_Vector_Spaces.thy
changeset 60422 be7565a1115b
parent 60307 75e1aa7a450e
child 60758 d8d85a8172b5
equal deleted inserted replaced
60421:92d9557fb78c 60422:be7565a1115b