changeset 36778 | 739a9379e29b |
parent 32479 | 521cc9bf2958 |
child 57514 | bdc2c6b40bf2 |
--- a/src/HOL/ex/Sqrt_Script.thy Sun May 09 17:47:43 2010 -0700 +++ b/src/HOL/ex/Sqrt_Script.thy Sun May 09 22:51:11 2010 -0700 @@ -61,7 +61,7 @@ apply (rule notI) apply (erule Rats_abs_nat_div_natE) apply (simp del: real_of_nat_mult - add: real_abs_def divide_eq_eq prime_not_square real_of_nat_mult [symmetric]) + add: abs_if divide_eq_eq prime_not_square real_of_nat_mult [symmetric]) done lemmas two_sqrt_irrational =