src/HOL/Analysis/Euclidean_Space.thy
changeset 81025 d4eb94b46e83
parent 80914 d97fdabd9e2b
child 81142 6ad2c917dd2e