src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
changeset 54260 6a967667fd45
parent 54258 adfc759263ab
child 55522 23d2cbac6dce
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 05 09:44:59 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 05 09:44:59 2013 +0100
@@ -1209,7 +1209,7 @@
   apply (subst inf_commute)
   apply (subst SUP_inf)
   apply (intro SUP_cong[OF refl])
-  apply (cut_tac A="ball x b - {x}" and B="{x}" and M=f in INF_union)
+  apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
   apply (simp add: INF_def del: inf_ereal_def)
   done