src/HOL/Rational.thy

 proof -
   from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def)
   then show ?thesis by (simp add: mult_rat [symmetric])
 qed
 
-primrec power_rat
-where
-  "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 r :: rat show "q * r = r * q"

 next
   show "(0::rat) \<noteq> 1" by (simp add: Zero_rat_def One_rat_def eq_rat)
 next
   fix q :: rat show "q * 1 = q"
     by (cases q) (simp add: One_rat_def 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]
+qed
 
 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)

 begin
 
 definition
   rat_number_of_def [code del]: "number_of w = Fract w 1"
 
-instance by intro_classes (simp add: rat_number_of_def of_int_rat)
+instance proof
+qed (simp add: rat_number_of_def of_int_rat)
 
 end
 
 lemma rat_number_collapse [code post]:
   "Fract 0 k = 0"