remove duplicate instance declaration
authorhuffman
Sun, 22 Feb 2009 08:52:44 -0800
changeset 30066 9223483cc927
parent 30053 044308b4948a
child 30067 84205156ca8a
remove duplicate instance declaration
src/HOL/Library/Euclidean_Space.thy
--- 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