src/HOL/Numeral_Simprocs.thy
changeset 37886 2f9d3fc1a8ac
parent 33366 b0096ac3b731
child 45284 ae78a4ffa81d
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Mon Jul 19 16:09:43 2010 +0200
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Mon Jul 19 16:09:44 2010 +0200
     1.3 @@ -92,7 +92,6 @@
     1.4       "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
     1.5  by (simp add: nat_mult_div_cancel1)
     1.6  
     1.7 -
     1.8  use "Tools/numeral_simprocs.ML"
     1.9  
    1.10  use "Tools/nat_numeral_simprocs.ML"
    1.11 @@ -117,4 +116,4 @@
    1.12    #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
    1.13  *}
    1.14  
    1.15 -end
    1.16 \ No newline at end of file
    1.17 +end