src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 48048 87b94fb75198
parent 47108 2a1953f0d20d
child 48125 602dc0215954
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu May 31 10:01:15 2012 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu May 31 10:05:07 2012 +0200
     1.3 @@ -1760,7 +1760,7 @@
     1.4      hence "norm (a + x) \<le> b + norm a" using norm_triangle_ineq[of a x] b by auto
     1.5    }
     1.6    thus ?thesis unfolding bounded_pos using norm_ge_zero[of a] b(1) using add_strict_increasing[of b 0 "norm a"]
     1.7 -    by (auto intro!: add exI[of _ "b + norm a"])
     1.8 +    by (auto intro!: exI[of _ "b + norm a"])
     1.9  qed
    1.10  
    1.11