src/HOL/Library/Euclidean_Space.thy
changeset 30066 9223483cc927
parent 30045 b8ddd7667eed
child 30242 aea5d7fa7ef5
child 30303 9c4f4ac0d038
--- 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