src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 68983 caedabd2771c
parent 68833 fde093888c16
child 69000 7cb3ddd60fd6
equal deleted inserted replaced
68980:5717fbc55521 68983:caedabd2771c