# HG changeset patch
# User haftmann
# Date 1268319155 -3600
# Node ID 3b17dff14c4f8ba4ae6ecae6f4406138bccba51b
# Parent  1bdaa24fb56daadf3ab1eaca28425a1eafc110f0
tuned prefix of ac rules

diff -r 1bdaa24fb56d -r 3b17dff14c4f src/HOL/ex/Summation.thy
--- a/src/HOL/ex/Summation.thy	Thu Mar 11 15:52:35 2010 +0100
+++ b/src/HOL/ex/Summation.thy	Thu Mar 11 15:52:35 2010 +0100
@@ -10,7 +10,7 @@
 
 lemma add_setsum_orient:
   "setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"
-  by (fact plus.commute)
+  by (fact add.commute)
 
 lemma add_setsum_int:
   fixes j k l :: int