(* Title: HOL/Real/HahnBanach/ROOT.ML ID: $Id$ Author: Gertrud Bauer, TU Munich The Hahn-Banach theorem for real vector spaces (Isabelle/Isar). *) time_use_thy "Bounds"; time_use_thy "HahnBanach";