| author | wenzelm |
| Fri, 08 Mar 2002 16:24:06 +0100 | |
| changeset 13049 | ce180e5b7fa0 |
| parent 10752 | c4f1bf2acf4c |
| child 17260 | df7c3b1f390a |
| permissions | -rw-r--r-- |
|
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 | 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 |
|
|
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
7978
diff
changeset
|
8 |
with_path "../../Hyperreal" time_use_thy "HahnBanach"; |