# HG changeset patch
# User huffman
# Date 1234564914 28800
# Node ID 26ee9656872a2e078ebc9f1bda8b043cdcea1464
# Parent  856f16a3b43628de26116fa07b8bb4cc84f5a278
add instance for cancel_comm_monoid_add

diff -r 856f16a3b436 -r 26ee9656872a src/HOL/Library/Euclidean_Space.thy
--- 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)