tuned prefix of ac rules
authorhaftmann
Thu Mar 11 15:52:35 2010 +0100 (2010-03-11)
changeset 357323b17dff14c4f
parent 35731 1bdaa24fb56d
child 35733 b57070d54cd5
tuned prefix of ac rules
src/HOL/ex/Summation.thy
     1.1 --- a/src/HOL/ex/Summation.thy	Thu Mar 11 15:52:35 2010 +0100
     1.2 +++ b/src/HOL/ex/Summation.thy	Thu Mar 11 15:52:35 2010 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  lemma add_setsum_orient:
     1.6    "setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"
     1.7 -  by (fact plus.commute)
     1.8 +  by (fact add.commute)
     1.9  
    1.10  lemma add_setsum_int:
    1.11    fixes j k l :: int