author | haftmann |
Mon, 26 Oct 2009 09:03:57 +0100 | |
changeset 33176 | d6936fd7cda8 |
parent 31795 | be3e1cc5005c |
child 33615 | 261abc2e3155 |
permissions | -rw-r--r-- |
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset
|
1 |
(* Title: HOL/Hahn_Banach/ROOT.ML |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
2 |
Author: Gertrud Bauer, TU Munich |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
3 |
|
7927 | 4 |
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
|
5 |
*) |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
6 |
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset
|
7 |
use_thy "Hahn_Banach"; |