src/HOL/Real/HahnBanach/ROOT.ML
author wenzelm
Fri Oct 29 20:18:34 1999 +0200 (1999-10-29)
changeset 7978 1b99ee57d131
parent 7927 b50446a33c16
child 10752 c4f1bf2acf4c
permissions -rw-r--r--
final 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@7535
     8
time_use_thy "HahnBanach";