src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 70299 83774d669b51
parent 70196 b7ef9090feed
child 70378 ebd108578ab1