src/HOL/Analysis/Abstract_Euclidean_Space.thy
changeset 70027 94494b92d8d0
parent 70019 095dce9892e8
child 70086 72c52a897de2