src/HOL/Rational.thy

   then show ?thesis by (simp add: mult_rat [symmetric])
 qed
 
 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)" 
     by (cases q, cases r, cases s) (simp add: eq_rat)
 next

   fix q :: rat
   fix n :: nat
   show "q ^ 0 = 1" by simp
   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"
   by (induct k) (simp_all add: Zero_rat_def One_rat_def)

    = of_rat a / of_rat b"
 by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
 
 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)
 apply (simp add: of_rat_rat eq_rat)
 apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)