src/HOL/Real_Vector_Spaces.thy
changeset 57637 eeb2d50ec71f
parent 57514 bdc2c6b40bf2
child 58889 5b7a9633cfa8
equal deleted inserted replaced
57636:3ab503b04bdb 57637:eeb2d50ec71f