src/HOL/Hahn_Banach/ROOT.ML

"no_atp" fact that leads to unsound proofs

(*  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"];