src/HOL/Hahn_Banach/Hahn_Banach_Lemmas.thy
changeset 36485 56ce8fc56be3
parent 31795 be3e1cc5005c
child 62390 842917225d56
equal deleted inserted replaced
36484:134ac130a8ed 36485:56ce8fc56be3