src/HOL/Library/Euclidean_Space.thy
changeset 30960 fec1a04b7220
parent 30665 4cf38ea4fad2
child 31021 53642251a04f
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Wed Apr 22 19:09:19 2009 +0200
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Wed Apr 22 19:09:21 2009 +0200
     1.3 @@ -253,12 +253,7 @@
     1.4    "vector_power x 0 = 1"
     1.5    | "vector_power x (Suc n) = x * vector_power x n"
     1.6  
     1.7 -instantiation "^" :: (recpower,type) recpower
     1.8 -begin
     1.9 -  definition vec_power_def: "op ^ \<equiv> vector_power"
    1.10 -  instance
    1.11 -  apply (intro_classes) by (simp_all add: vec_power_def)
    1.12 -end
    1.13 +instance "^" :: (recpower,type) recpower ..
    1.14  
    1.15  instance "^" :: (semiring,type) semiring
    1.16    apply (intro_classes) by (vector ring_simps)+