src/HOL/Analysis/Euclidean_Space.thy
changeset 68976 105bbce656a5
parent 68620 707437105595
child 69064 5840724b1d71