src/HOL/Hahn_Banach/ROOT.ML

remove redundant lemma word_sub_def

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