src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 82265 4b875a4c83b0
parent 81128 5b201b24d99b
child 82518 da14e77a48b2