(* Title: HOL/Hahn_Banach/ROOT.ML Author: Gertrud Bauer, TU Munich The Hahn-Banach theorem for real vector spaces (Isabelle/Isar). *) use_thys ["Hahn_Banach"];