src/HOL/Real_Vector_Spaces.thy
changeset 58585 efc8b2c54a38
parent 57514 bdc2c6b40bf2
child 58889 5b7a9633cfa8
equal deleted inserted replaced
58584:b6492a7abb59 58585:efc8b2c54a38