src/HOL/Rational.thy
changeset 30273 ecd6f0ca62ea
parent 30242 aea5d7fa7ef5
child 30649 57753e0ec1d4
     1.1 --- a/src/HOL/Rational.thy	Thu Mar 05 00:16:28 2009 +0100
     1.2 +++ b/src/HOL/Rational.thy	Wed Mar 04 17:12:23 2009 -0800
     1.3 @@ -158,8 +158,8 @@
     1.4  
     1.5  primrec power_rat
     1.6  where
     1.7 -  rat_power_0:     "q ^ 0 = (1\<Colon>rat)"
     1.8 -  | rat_power_Suc: "q ^ Suc n = (q\<Colon>rat) * (q ^ n)"
     1.9 +  "q ^ 0 = (1\<Colon>rat)"
    1.10 +| "q ^ Suc n = (q\<Colon>rat) * (q ^ n)"
    1.11  
    1.12  instance proof
    1.13    fix q r s :: rat show "(q * r) * s = q * (r * s)" 
    1.14 @@ -200,6 +200,8 @@
    1.15    show "q ^ (Suc n) = q * (q ^ n)" by simp
    1.16  qed
    1.17  
    1.18 +declare power_rat.simps [simp del]
    1.19 +
    1.20  end
    1.21  
    1.22  lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
    1.23 @@ -666,7 +668,7 @@
    1.24  
    1.25  lemma of_rat_power:
    1.26    "(of_rat (a ^ n)::'a::{field_char_0,recpower}) = of_rat a ^ n"
    1.27 -by (induct n) (simp_all add: of_rat_mult power_Suc)
    1.28 +by (induct n) (simp_all add: of_rat_mult)
    1.29  
    1.30  lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)"
    1.31  apply (induct a, induct b)