src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 73057 45a34cc581b8
parent 72643 6b3599ff0687
child 73791 e10d530f157a