# HG changeset patch
# User huffman
# Date 1380060229 25200
# Node ID e6cb01686f7bc1b594dd9951fb1a6dc6adcdbc68
# Parent  60b89c05317fbe48e183729f603bb05c98047d77
replace lemma with more general simp rule

diff -r 60b89c05317f -r e6cb01686f7b src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 23:51:32 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 15:03:49 2013 -0700
@@ -1485,9 +1485,6 @@
 
 text{* The expected monotonicity property. *}
 
-lemma Lim_within_empty: "(f ---> l) (at x within {})"
-  unfolding tendsto_def eventually_at_filter by simp
-
 lemma Lim_Un:
   assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
   shows "(f ---> l) (at x within (S \<union> T))"
@@ -1551,7 +1548,7 @@
   shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
 proof (cases "{x<..} \<inter> I = {}")
   case True
-  then show ?thesis by (simp add: Lim_within_empty)
+  then show ?thesis by simp
 next
   case False
   show ?thesis
diff -r 60b89c05317f -r e6cb01686f7b src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Sep 24 23:51:32 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy	Tue Sep 24 15:03:49 2013 -0700
@@ -490,7 +490,7 @@
     unfolding le_filter_def eventually_Sup by simp }
   { show "Inf {} = (top::'a filter)"
     by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
-      (metis (full_types) Topological_Spaces.top_filter_def always_eventually eventually_top) }
+      (metis (full_types) top_filter_def always_eventually eventually_top) }
   { show "Sup {} = (bot::'a filter)"
     by (auto simp: bot_filter_def Sup_filter_def) }
 qed
@@ -754,6 +754,9 @@
 lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
   unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
 
+lemma at_within_empty [simp]: "at a within {} = bot"
+  unfolding at_within_def by simp
+
 lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
   unfolding trivial_limit_def eventually_at_topological
   by (safe, case_tac "S = {a}", simp, fast, fast)