diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- 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"