src/HOL/Topological_Spaces.thy

     and continuous_on_Icc_at_leftD: "(f \<longlongrightarrow> f b) (at_left b)"
   using assms
   by (auto simp: at_within_Icc_at_right at_within_Icc_at_left continuous_on_def
       dest: bspec[where x=a] bspec[where x=b])
 
-lemma continuous_on_discrete [simp, continuous_intros]:
+lemma continuous_on_discrete [simp]:
   "continuous_on A (f :: 'a :: discrete_topology \<Rightarrow> _)"
   by (auto simp: continuous_on_def at_discrete)
 
 subsubsection \<open>Continuity at a point\<close>
 

 
 lemma continuous_on_eq_continuous_within:
   "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. continuous (at x within s) f)"
   unfolding continuous_on_def continuous_within ..
 
-lemma continuous_discrete [simp, continuous_intros]:
+lemma continuous_discrete [simp]:
   "continuous (at x within A) (f :: 'a :: discrete_topology \<Rightarrow> _)"
   by (auto simp: continuous_def at_discrete)
 
 abbreviation isCont :: "('a::t2_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> bool"
   where "isCont f a \<equiv> continuous (at a) f"