src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 73013 d4b67dc6f4eb
parent 72643 6b3599ff0687
child 73791 e10d530f157a