src/HOL/Real_Vector_Spaces.thy
changeset 81577 a712bf5ccab0
parent 80932 261cd8722677
child 82080 0aa2d1c132b2
equal deleted inserted replaced
81576:0a01bec9bc13 81577:a712bf5ccab0