src/HOL/Real/HahnBanach/HahnBanachLemmas.thy
changeset 21346 c8aa120fa05d
parent 16417 9bc16273c2d4
equal deleted inserted replaced
21345:a18e60f597b6 21346:c8aa120fa05d