src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 70240 c73c8fd4b64c
parent 70196 b7ef9090feed
child 70378 ebd108578ab1