src/HOL/Multivariate_Analysis/Euclidean_Space.thy
changeset 42230 594480d25aaa
parent 41969 1cf3e4107a2a
child 42814 5af15f1e2ef6