| changeset 16417 | 9bc16273c2d4 |
| parent 15206 | 09d78ec709c7 |
| child 19931 | fb32b43e7f80 |
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri Jun 17 16:12:49 2005 +0200 @@ -5,7 +5,7 @@ header {* The norm of a function *} -theory FunctionNorm = NormedSpace + FunctionOrder: +theory FunctionNorm imports NormedSpace FunctionOrder begin subsection {* Continuous linear forms*}