src/HOL/Hahn_Banach/ROOT.ML

more accurate dependencies;
tuned;

(*  Title:      HOL/Hahn_Banach/ROOT.ML
    Author:     Gertrud Bauer, TU Munich

The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
*)

use_thy "Hahn_Banach";