src/HOL/Multivariate_Analysis/Euclidean_Space.thy
changeset 33365 4db1b31b246e
parent 33270 320a1d67b9ae
child 33714 eb2574ac4173