src/HOL/Analysis/Abstract_Euclidean_Space.thy
changeset 70805 c39bd607203b
parent 70097 4005298550a6
child 70817 dd675800469d
equal deleted inserted replaced
70804:4eef7c6ef7bf 70805:c39bd607203b