| changeset 31494 | 1ba61c7b129f |
| parent 31492 | 5400beeddb55 |
| child 31564 | d2abf6f6f619 |
--- a/src/HOL/RealVector.thy Sun Jun 07 19:38:32 2009 -0700 +++ b/src/HOL/RealVector.thy Sun Jun 07 20:57:24 2009 -0700 @@ -419,7 +419,7 @@ subsection {* Topological spaces *} class "open" = - fixes "open" :: "'a set set" + fixes "open" :: "'a set \<Rightarrow> bool" class topological_space = "open" + assumes open_UNIV [simp, intro]: "open UNIV"