author  wenzelm 
Mon, 25 Oct 1999 19:24:43 +0200  
changeset 7927  b50446a33c16 
parent 7808  fd019ac3485f 
child 7978  1b99ee57d131 
permissions  rwrr 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/Real/HahnBanach/ROOT.ML 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

3 
Author: Gertrud Bauer, TU Munich 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

4 

7927  5 
The HahnBanach theorem for real vector spaces (Isabelle/Isar). 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

6 
*) 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

7 

7808  8 
time_use_thy "Bounds"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

9 
time_use_thy "HahnBanach"; 