src/HOL/Hahn_Banach/Bounds.thy
changeset 71388 57861bd0a3e1
parent 66453 cc19f7ca2ed6
child 80914 d97fdabd9e2b