src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 69519 0563419bf022
parent 69508 2a4c8a2a3f8e
child 69631 6c3e6038e74c
equal deleted inserted replaced
69518:bf88364c9e94 69519:0563419bf022