src/HOL/Analysis/Euclidean_Space.thy
changeset 70045 7b6add80e3a5
parent 69597 ff784d5a5bfb
child 70136 f03a01a18c6e