changeset 41413 | 64cd30d6b0b8 |
parent 37887 | 2ae085b07f2f |
child 44887 | 7ca82df6e951 |
--- a/src/HOL/Hahn_Banach/Vector_Space.thy Wed Dec 29 13:51:17 2010 +0100 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy Wed Dec 29 17:34:41 2010 +0100 @@ -5,7 +5,7 @@ header {* Vector spaces *} theory Vector_Space -imports Real Bounds Zorn +imports Real Bounds "~~/src/HOL/Library/Zorn" begin subsection {* Signature *}