src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 69467 e8893c893241
parent 69272 15e9ed5b28fb
child 69508 2a4c8a2a3f8e
equal deleted inserted replaced
69466:796e01aba901 69467:e8893c893241