src/HOL/Real_Vector_Spaces.thy
changeset 61841 4d3527b94f2a
parent 61799 4cf66f21b764
child 61915 e9812a95d108
equal deleted inserted replaced
61840:a3793600cb93 61841:4d3527b94f2a