src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
changeset 51481 ef949192e5d6
parent 51475 ebf9d4fd00ba
child 51530 609914f0934a
     1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -470,7 +470,7 @@
     1.4    fixes f :: "'a::t2_space => real"
     1.5    fixes A assumes "open A"
     1.6    shows "continuous_on A f <-> continuous_on A (ereal o f)"
     1.7 -  using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at)
     1.8 +  using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at cong del: continuous_on_cong)
     1.9  
    1.10  
    1.11  lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>::ereal)}) real"