Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 63492 a662e8139804
parent 63469 b6900858dcb9
child 63540 f8652d0534fa 
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jul 14 12:21:12 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jul 14 14:48:49 2016 +0100
@@ -819,7 +819,7 @@
   apply (auto simp add: istopology_def)
   done
 
-lemma topspace_euclidean: "topspace euclidean = UNIV"
+lemma topspace_euclidean [simp]: "topspace euclidean = UNIV"
   apply (simp add: topspace_def)
   apply (rule set_eqI)
   apply (auto simp add: open_openin[symmetric])
isabelle