src/HOL/Real_Vector_Spaces.thy
changeset 66200 02c66b71c013
parent 66089 def95e0bc529
child 66420 bc0dab0e7b40
equal deleted inserted replaced
66198:4a5589dd8e1a 66200:02c66b71c013