# HG changeset patch # User haftmann # Date 1279548584 -7200 # Node ID 2f9d3fc1a8ac341361f2fa38f4f3cd68209e16d9 # Parent c43805c80eb6c8ea194d0bba905d89032ae34ea0 tuned whitespace diff -r c43805c80eb6 -r 2f9d3fc1a8ac src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Mon Jul 19 16:09:43 2010 +0200 +++ b/src/HOL/Numeral_Simprocs.thy Mon Jul 19 16:09:44 2010 +0200 @@ -92,7 +92,6 @@ "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)" by (simp add: nat_mult_div_cancel1) - use "Tools/numeral_simprocs.ML" use "Tools/nat_numeral_simprocs.ML" @@ -117,4 +116,4 @@ #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals)) *} -end \ No newline at end of file +end