--- a/src/HOL/Library/Euclidean_Space.thy Fri Feb 13 14:12:00 2009 -0800
+++ b/src/HOL/Library/Euclidean_Space.thy Fri Feb 13 14:41:54 2009 -0800
@@ -236,6 +236,7 @@
apply (intro_classes) by (vector ring_simps)+
instance "^" :: (comm_semiring_0,type) comm_semiring_0 by (intro_classes)
+instance "^" :: (cancel_comm_monoid_add, type) cancel_comm_monoid_add ..
instance "^" :: (semiring_0_cancel,type) semiring_0_cancel by (intro_classes)
instance "^" :: (comm_semiring_0_cancel,type) comm_semiring_0_cancel by (intro_classes)
instance "^" :: (ring,type) ring by (intro_classes)