1 (* Title: HOL/Hahn_Banach/ROOT.ML
2 Author: Gertrud Bauer, TU Munich
3
4 The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
5 *)
6
7 use_thy "Hahn_Banach";