src/HOL/Hahn_Banach/Hahn_Banach.thy
changeset 71751 abf3e80bd815
parent 65166 f8aafbf2b02e
child 76987 4c275405faae