src/HOL/Multivariate_Analysis/Euclidean_Space.thy
changeset 38316 88e774d09fbc
parent 38136 bd4965bb7bdc
child 38642 8fa437809c67