src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 82351 882b80bd10c8
parent 80914 d97fdabd9e2b
child 82603 5648293625a5
equal deleted inserted replaced
82350:00b59ba22c01 82351:882b80bd10c8