--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed May 17 01:23:41 2006 +0200
@@ -9,12 +9,10 @@
imports Gauss
begin
-(***************************************************************)
-(* *)
-(* Lemmas leading up to the proof of theorem 3.3 in *)
-(* Niven and Zuckerman's presentation *)
-(* *)
-(***************************************************************)
+text {*
+ Lemmas leading up to the proof of theorem 3.3 in Niven and
+ Zuckerman's presentation.
+*}
lemma (in GAUSS) QRLemma1: "a * setsum id A =
p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E"
@@ -149,11 +147,8 @@
apply (auto simp add: GAUSS_def)
done
-(******************************************************************)
-(* *)
-(* Stuff about S, S1 and S2... *)
-(* *)
-(******************************************************************)
+
+subsection {* Stuff about S, S1 and S2 *}
locale QRTEMP =
fixes p :: "int"