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;
     1 (*  Title:      HOL/Real/HahnBanach/ROOT.ML
     2     ID:         $Id$
     3     Author:     Gertrud Bauer, TU Munich
     4 
     5 The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
     6 *)
     7 
     8 time_use_thy "Bounds";
     9 time_use_thy "HahnBanach";