src/HOL/Decision_Procs/Rat_Pair.thy
changeset 58834 773b378d9313
parent 57512 cc97b347b301
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Oct 30 16:36:44 2014 +0000
     1.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Oct 30 21:02:01 2014 +0100
     1.3 @@ -211,11 +211,7 @@
     1.4  
     1.5  lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
     1.6      (of_int(n div d)::'a::field_char_0) = of_int n / of_int d"
     1.7 -  apply (frule of_int_div_aux [of d n, where ?'a = 'a])
     1.8 -  apply simp
     1.9 -  apply (simp add: dvd_eq_mod_eq_0)
    1.10 -  done
    1.11 -
    1.12 +  using of_int_div_aux [of d n, where ?'a = 'a] by simp
    1.13  
    1.14  lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
    1.15  proof -