src/HOL/Numeral_Simprocs.thy
changeset 59757 93d4169e07dc
parent 58889 5b7a9633cfa8
child 59867 58043346ca64
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Thu Mar 19 14:25:32 2015 +0000
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Fri Mar 20 14:00:22 2015 +0000
     1.3 @@ -99,6 +99,10 @@
     1.4    shows "(k * m) div (k * n) = (if k = 0 then 0 else m div n)"
     1.5    by (fact div_mult_mult1_if)
     1.6  
     1.7 +lemma numeral_times_minus_swap:
     1.8 +  fixes x:: "'a::comm_ring_1" shows  "numeral w * -x = x * - numeral w"
     1.9 +  by (simp add: mult.commute)
    1.10 +
    1.11  ML_file "Tools/numeral_simprocs.ML"
    1.12  
    1.13  simproc_setup semiring_assoc_fold