src/HOL/Analysis/Euclidean_Space.thy
changeset 68535 4d09df93d1a2
parent 68310 d0a7ddf5450e
child 68617 75129a73aca3