src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 73282 dcadb3243cfa
parent 72643 6b3599ff0687
child 73791 e10d530f157a
equal deleted inserted replaced
73281:22417b631453 73282:dcadb3243cfa