src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 82313 df99e867c63e
parent 81128 5b201b24d99b
child 82518 da14e77a48b2
equal deleted inserted replaced
82311:a3b556a23541 82313:df99e867c63e