src/HOL/Real/HahnBanach/ROOT.ML
author wenzelm
Fri Sep 10 17:28:51 1999 +0200 (1999-09-10)
changeset 7535 599d3414b51d
child 7808 fd019ac3485f
permissions -rw-r--r--
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
(by Gertrud Bauer, TU Munich);
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@7535
     5
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
wenzelm@7535
     6
*)
wenzelm@7535
     7
wenzelm@7535
     8
time_use_thy "HahnBanach";