src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 71606 b3b0d87edd20
parent 71025 be8cec1abcbb
child 71633 07bec530f02e