# HG changeset patch
# User huffman
# Date 1338451507 -7200
# Node ID 87b94fb75198c822454a28be11be22b6146e3e6f
# Parent  2efdcc7d0775fb112d23fac9387c9a5b3dfe9c1e
remove stray reference to no-longer-existing theorem 'add'

diff -r 2efdcc7d0775 -r 87b94fb75198 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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