src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
changeset 21964 df2e82888a66
parent 16417 9bc16273c2d4
child 23378 1d138d6bb461