src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
changeset 82003 abb40413c1e7
parent 81464 2575f1bd226b
equal deleted inserted replaced
82002:150bbde003ef 82003:abb40413c1e7