author | huffman |
Sun, 22 Feb 2009 08:52:44 -0800 | |
changeset 30066 | 9223483cc927 |
parent 30053 | 044308b4948a |
child 30067 | 84205156ca8a |
--- a/src/HOL/Library/Euclidean_Space.thy Sun Feb 22 11:30:57 2009 +0100 +++ b/src/HOL/Library/Euclidean_Space.thy Sun Feb 22 08:52:44 2009 -0800 @@ -1010,11 +1010,6 @@ lemma dist_le_0: "dist x y <= 0 \<longleftrightarrow> x = y" by norm -instantiation "^" :: (monoid_add,type) monoid_add -begin - instance by (intro_classes) -end - lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)" apply vector apply auto