| changeset 30663 | 0b6aff7451b2 |
| parent 30067 | 84205156ca8a |
| child 30729 | 461ee3e49ad3 |
--- a/src/HOL/Library/Inner_Product.thy Mon Mar 23 08:14:23 2009 +0100 +++ b/src/HOL/Library/Inner_Product.thy Mon Mar 23 08:14:24 2009 +0100 @@ -5,7 +5,7 @@ header {* Inner Product Spaces and the Gradient Derivative *} theory Inner_Product -imports Complex FrechetDeriv +imports Complex_Main FrechetDeriv begin subsection {* Real inner product spaces *}