src/HOL/Complex.thy
changeset 30273 ecd6f0ca62ea
parent 29667 53103fc8ffa3
child 30729 461ee3e49ad3
     1.1 --- a/src/HOL/Complex.thy	Thu Mar 05 00:16:28 2009 +0100
     1.2 +++ b/src/HOL/Complex.thy	Wed Mar 04 17:12:23 2009 -0800
     1.3 @@ -163,10 +163,13 @@
     1.4  begin
     1.5  
     1.6  primrec power_complex where
     1.7 -  complexpow_0:     "z ^ 0     = (1\<Colon>complex)"
     1.8 -  | complexpow_Suc: "z ^ Suc n = (z\<Colon>complex) * z ^ n"
     1.9 +  "z ^ 0     = (1\<Colon>complex)"
    1.10 +| "z ^ Suc n = (z\<Colon>complex) * z ^ n"
    1.11  
    1.12 -instance by intro_classes simp_all
    1.13 +instance proof
    1.14 +qed simp_all
    1.15 +
    1.16 +declare power_complex.simps [simp del]
    1.17  
    1.18  end
    1.19