src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 68586 006da53a8ac1
parent 68239 0764ee22a4d1
child 68833 fde093888c16