src/HOL/Real/HahnBanach/HahnBanachLemmas.thy
changeset 9257 ea5b59af6b31
child 9394 1ff8a6234c6a
equal deleted inserted replaced
9256:f9a6670427fb 9257:ea5b59af6b31
       
     1 
       
     2 theory HahnBanachLemmas = HahnBanachSupLemmas + HahnBanachExtLemmas:;
       
     3 end;