src/HOL/Real/HahnBanach/ROOT.ML
author wenzelm
Mon Oct 25 19:24:43 1999 +0200 (1999-10-25)
changeset 7927 b50446a33c16
parent 7808 fd019ac3485f
child 7978 1b99ee57d131
permissions -rw-r--r--
update by Gertrud Bauer;
wenzelm@7535
     1
(*  Title:      HOL/Real/HahnBanach/ROOT.ML
wenzelm@7535
     2
    ID:         $Id$
wenzelm@7535
     3
    Author:     Gertrud Bauer, TU Munich
wenzelm@7535
     4
wenzelm@7927
     5
The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
wenzelm@7535
     6
*)
wenzelm@7535
     7
wenzelm@7808
     8
time_use_thy "Bounds";
wenzelm@7535
     9
time_use_thy "HahnBanach";