src/HOL/Analysis/Euclidean_Space.thy
changeset 68743 91162dd89571
parent 68620 707437105595
child 69064 5840724b1d71