changeset 51002 | 496013a6eb38 |
parent 50880 | b22ecedde1c7 |
child 52143 | 36ffe23b25f8 |
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Jan 31 12:09:07 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Jan 31 17:42:12 2013 +0100 @@ -387,9 +387,6 @@ instance proof fix a :: real and x y :: "'a ^ 'b" - show "0 \<le> norm x" - unfolding norm_vec_def - by (rule setL2_nonneg) show "norm x = 0 \<longleftrightarrow> x = 0" unfolding norm_vec_def by (simp add: setL2_eq_0_iff vec_eq_iff)