# HG changeset patch
# User huffman
# Date 1235321564 28800
# Node ID 9223483cc92706def81300094b750374468dc921
# Parent  044308b4948aaf2eb58822c3e70755cf1cbc1172
remove duplicate instance declaration

diff -r 044308b4948a -r 9223483cc927 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