--- a/src/HOL/Rational.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Rational.thy Wed Apr 22 19:09:21 2009 +0200
@@ -156,11 +156,6 @@
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)
@@ -193,15 +188,8 @@
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]
-
end
lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
@@ -222,7 +210,8 @@
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