src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 73439 cb127ce2c092
parent 72643 6b3599ff0687
child 73791 e10d530f157a