# HG changeset patch
# User wenzelm
# Date 1322167318 -3600
# Node ID a0336f8b65587da4d5a5e8fd0c75937fb558f6a9
# Parent  b4f374a45668e6b6acea27f95d4c24bd259e8888
speed-up proof;

diff -r b4f374a45668 -r a0336f8b6558 src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Thu Nov 24 21:15:20 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Thu Nov 24 21:41:58 2011 +0100
@@ -114,8 +114,8 @@
    (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
 proof -
   assume "a \<in> zOdd"
-  from QRLemma4 [OF this] have
-    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" ..
+  from QRLemma4 [OF this, symmetric] have
+    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" .
   moreover have "0 \<le> int(card E)"
     by auto
   moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"