src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 81920 8d5989ab1e42
parent 81128 5b201b24d99b
child 82518 da14e77a48b2
equal deleted inserted replaced
81919:f4cd3e679096 81920:8d5989ab1e42