src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 78727 1b052426a2b7
parent 78475 a5f6d2fc1b1f
child 80914 d97fdabd9e2b
equal deleted inserted replaced
78726:810eca753919 78727:1b052426a2b7