src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 68004 a8a20be7053a
parent 67981 349c639e593c
child 68120 2f161c6910f7