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)
```