src/HOL/Real_Vector_Spaces.thy
changeset 64899 749d3a86c6a3
parent 64788 19f3d4af7a7d
child 65036 ab7e11730ad8
equal deleted inserted replaced
64898:49aa13b1b592 64899:749d3a86c6a3