src/HOL/Real_Vector_Spaces.thy
changeset 68300 cd8ab1a7a286
parent 68072 493b818e8e10
child 68397 cace81744c61
equal deleted inserted replaced
68299:0b5a23477911 68300:cd8ab1a7a286