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