# 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..