src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 77210 1ffee8893b12
parent 76724 7ff71bdcf731
child 77223 607e1e345e8f