src/HOL/Hahn_Banach/Normed_Space.thy
changeset 45284 ae78a4ffa81d
parent 44887 7ca82df6e951
child 46867 0883804b67bb