src/HOL/Library/Float.thy
changeset 59984 4f1eccec320c
parent 59554 4044f53326c9
child 60017 b785d6d06430
     1.1 --- a/src/HOL/Library/Float.thy	Wed Apr 08 23:00:09 2015 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Thu Apr 09 09:12:47 2015 +0200
     1.3 @@ -1093,9 +1093,9 @@
     1.4    by (cases "b=0") (simp_all add: div_mult2_eq[symmetric] ac_simps)
     1.5  
     1.6  lemma real_div_nat_eq_floor_of_divide:
     1.7 -  fixes a b::nat
     1.8 -  shows "a div b = real (floor (a/b))"
     1.9 -by (metis floor_divide_eq_div real_of_int_of_nat_eq zdiv_int)
    1.10 +  fixes a b :: nat
    1.11 +  shows "a div b = real \<lfloor>a / b\<rfloor>"
    1.12 +  by (simp add: floor_divide_of_nat_eq [of a b] real_eq_of_nat)
    1.13  
    1.14  definition "rat_precision prec x y = int prec - (bitlen x - bitlen y)"
    1.15