src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 54259 71c701dc5bf9
parent 54258 adfc759263ab
child 54260 6a967667fd45
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:44:58 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:44:59 2013 +0100
     1.3 @@ -2686,7 +2686,7 @@
     1.4  lemma Inf_insert:
     1.5    fixes S :: "real set"
     1.6    shows "bounded S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
     1.7 -  by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_if)
     1.8 +  by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_If)
     1.9  
    1.10  lemma Inf_insert_finite:
    1.11    fixes S :: "real set"