src/HOL/Library/Euclidean_Space.thy
changeset 29905 26ee9656872a
parent 29881 58f3c48dbbb7
child 29906 80369da39838
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Fri Feb 13 14:12:00 2009 -0800
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Fri Feb 13 14:41:54 2009 -0800
     1.3 @@ -236,6 +236,7 @@
     1.4    apply (intro_classes) by (vector ring_simps)+
     1.5  
     1.6  instance "^" :: (comm_semiring_0,type) comm_semiring_0 by (intro_classes) 
     1.7 +instance "^" :: (cancel_comm_monoid_add, type) cancel_comm_monoid_add ..
     1.8  instance "^" :: (semiring_0_cancel,type) semiring_0_cancel by (intro_classes) 
     1.9  instance "^" :: (comm_semiring_0_cancel,type) comm_semiring_0_cancel by (intro_classes) 
    1.10  instance "^" :: (ring,type) ring by (intro_classes)