--- a/src/HOL/Rational.thy Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Rational.thy Wed Mar 04 17:12:23 2009 -0800
@@ -158,8 +158,8 @@
primrec power_rat
where
- rat_power_0: "q ^ 0 = (1\<Colon>rat)"
- | rat_power_Suc: "q ^ Suc n = (q\<Colon>rat) * (q ^ n)"
+ "q ^ 0 = (1\<Colon>rat)"
+| "q ^ Suc n = (q\<Colon>rat) * (q ^ n)"
instance proof
fix q r s :: rat show "(q * r) * s = q * (r * s)"
@@ -200,6 +200,8 @@
show "q ^ (Suc n) = q * (q ^ n)" by simp
qed
+declare power_rat.simps [simp del]
+
end
lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
@@ -666,7 +668,7 @@
lemma of_rat_power:
"(of_rat (a ^ n)::'a::{field_char_0,recpower}) = of_rat a ^ n"
-by (induct n) (simp_all add: of_rat_mult power_Suc)
+by (induct n) (simp_all add: of_rat_mult)
lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)"
apply (induct a, induct b)