src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 45051 c478d1876371
parent 45031 9583f2b56f85
child 45270 d5b5c9259afd
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 22 13:17:14 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 22 14:12:16 2011 -0700
     1.3 @@ -5634,7 +5634,7 @@
     1.4      proof(cases "d = 0")
     1.5        case True
     1.6        have *: "\<And>x. ((1 - c) * x \<le> 0) = (x \<le> 0)" using `1 - c > 0`
     1.7 -        by (metis mult_zero_left real_mult_commute real_mult_le_cancel_iff1)
     1.8 +        by (metis mult_zero_left mult_commute real_mult_le_cancel_iff1)
     1.9        from True have "\<And>n. z n = z0" using cf_z2[of 0] and c unfolding z_def
    1.10          by (simp add: *)
    1.11        thus ?thesis using `e>0` by auto