src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 73691 2f9877db82a1
parent 72643 6b3599ff0687
child 73791 e10d530f157a