speed-up proof;
authorwenzelm
Thu Nov 24 21:41:58 2011 +0100 (2011-11-24)
changeset 45627a0336f8b6558
parent 45626 b4f374a45668
child 45628 f21eb7073895
speed-up proof;
src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
     1.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Thu Nov 24 21:15:20 2011 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Thu Nov 24 21:41:58 2011 +0100
     1.3 @@ -114,8 +114,8 @@
     1.4     (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
     1.5  proof -
     1.6    assume "a \<in> zOdd"
     1.7 -  from QRLemma4 [OF this] have
     1.8 -    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" ..
     1.9 +  from QRLemma4 [OF this, symmetric] have
    1.10 +    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" .
    1.11    moreover have "0 \<le> int(card E)"
    1.12      by auto
    1.13    moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"