| changeset 16417 | 9bc16273c2d4 |
| parent 15229 | 1eb23f805c06 |
| child 23378 | 1d138d6bb461 |
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri Jun 17 16:12:49 2005 +0200 @@ -5,7 +5,7 @@ header {* Extending non-maximal functions *} -theory HahnBanachExtLemmas = FunctionNorm: +theory HahnBanachExtLemmas imports FunctionNorm begin text {* In this section the following context is presumed. Let @{text E} be