changeset 14288 | d149e3cbdb39 |
parent 14051 | 4b61bbb0dcab |
child 15149 | c5c4884634b7 |
--- a/src/HOL/Complex/ex/Sqrt_Script.thy Wed Dec 10 14:29:44 2003 +0100 +++ b/src/HOL/Complex/ex/Sqrt_Script.thy Wed Dec 10 15:59:34 2003 +0100 @@ -68,8 +68,7 @@ apply clarify apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp) apply (simp del: real_of_nat_mult - add: real_divide_eq_eq prime_not_square - real_of_nat_mult [symmetric]) + add: divide_eq_eq prime_not_square real_of_nat_mult [symmetric]) done lemmas two_sqrt_irrational =