# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1536511212 -3600
# Node ID 1254f3e57fed3c7933e1b3adbf02343f87b59fd1
# Parent  ff6b594e4230b96ee7cff9d51e70b500e3186b83
Removed problematic rules from continuous_intros

diff -r ff6b594e4230 -r 1254f3e57fed src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Sun Sep 09 17:56:13 2018 +0200
+++ b/src/HOL/Topological_Spaces.thy	Sun Sep 09 17:40:12 2018 +0100
@@ -2116,7 +2116,7 @@
   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)
 
@@ -2162,7 +2162,7 @@
   "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)