src/HOL/Real/HahnBanach/FunctionNorm.thy
1999-09-21 wenzelm 1999-09-21 accomodate refined facts handling;
1999-09-10 wenzelm 1999-09-10 The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) (by Gertrud Bauer, TU Munich);