changeset 23365 | f31794033ae1 |
parent 23343 | 6a83ca5fe282 |
child 23429 | 5a55a9409e57 |
--- a/src/HOL/Real/Rational.thy Wed Jun 13 03:28:21 2007 +0200 +++ b/src/HOL/Real/Rational.thy Wed Jun 13 03:31:11 2007 +0200 @@ -565,7 +565,7 @@ by (induct n) (simp_all add: of_rat_add) lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z" -by (cases z rule: int_diff_cases', simp add: of_rat_diff) +by (cases z rule: int_diff_cases, simp add: of_rat_diff) lemma of_rat_number_of_eq [simp]: "of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})"