author | huffman |
Thu, 31 May 2012 10:05:07 +0200 | |
changeset 48048 | 87b94fb75198 |
parent 48047 | 2efdcc7d0775 |
child 48049 | d862b0d56c49 |
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu May 31 10:01:15 2012 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu May 31 10:05:07 2012 +0200 @@ -1760,7 +1760,7 @@ hence "norm (a + x) \<le> b + norm a" using norm_triangle_ineq[of a x] b by auto } thus ?thesis unfolding bounded_pos using norm_ge_zero[of a] b(1) using add_strict_increasing[of b 0 "norm a"] - by (auto intro!: add exI[of _ "b + norm a"]) + by (auto intro!: exI[of _ "b + norm a"]) qed