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