src/HOL/Real/HahnBanach/ZornLemma.thy
changeset 29251 8f84a608883d
parent 29234 60f7fb56f8cd