src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 69880 fe3c12990893
parent 69874 11065b70407d
child 69939 812ce526da33