| changeset 30663 | 0b6aff7451b2 |
| parent 29026 | 5fbaa05f637f |
| child 37765 | 26bdfb7b680b |
--- a/src/HOL/Library/ContNotDenum.thy Mon Mar 23 08:14:23 2009 +0100 +++ b/src/HOL/Library/ContNotDenum.thy Mon Mar 23 08:14:24 2009 +0100 @@ -5,7 +5,7 @@ header {* Non-denumerability of the Continuum. *} theory ContNotDenum -imports RComplete Hilbert_Choice +imports Complex_Main begin subsection {* Abstract *}