# HG changeset patch
# User nipkow
# Date 1109005468 -3600
# Node ID 206d779ba96df19675014462be2f8283743038dc
# Parent  fa23e05614266850ce74189a46351557aa45e8aa
fixed proof

diff -r fa23e0561426 -r 206d779ba96d src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Mon Feb 21 15:57:45 2005 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Mon Feb 21 18:04:28 2005 +0100
@@ -272,7 +272,7 @@
 
 lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
   apply (insert P_set_card Q_set_card P_set_finite Q_set_finite)
-  apply (auto simp add: S_def zmult_int setsum_constant_nat) 
+  apply (auto simp add: S_def zmult_int setsum_constant)
 done
 
 lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}"