Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix type of open
authorhuffman
Sun, 07 Jun 2009 20:57:24 -0700
changeset 31494 1ba61c7b129f
parent 31493 d92cfed6c6b2
child 31506 ff0ab207849a
fix type of open
src/HOL/RealVector.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle