src/HOL/Numeral_Simprocs.thy
changeset 37886 2f9d3fc1a8ac
parent 33366 b0096ac3b731
child 45284 ae78a4ffa81d
equal deleted inserted replaced
37885:c43805c80eb6 37886:2f9d3fc1a8ac
    90 
    90 
    91 lemma nat_mult_div_cancel_disj[simp]:
    91 lemma nat_mult_div_cancel_disj[simp]:
    92      "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
    92      "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
    93 by (simp add: nat_mult_div_cancel1)
    93 by (simp add: nat_mult_div_cancel1)
    94 
    94 
    95 
       
    96 use "Tools/numeral_simprocs.ML"
    95 use "Tools/numeral_simprocs.ML"
    97 
    96 
    98 use "Tools/nat_numeral_simprocs.ML"
    97 use "Tools/nat_numeral_simprocs.ML"
    99 
    98 
   100 declaration {* 
    99 declaration {*