src/HOL/Real_Vector_Spaces.thy
changeset 66008 010698325e36
parent 65680 378a2f11bec9
child 66089 def95e0bc529