diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -168,25 +168,31 @@
 begin
 
 definition
-  P_set :: "int set"
+  P_set :: "int set" where
   "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
 
-  Q_set :: "int set"
+definition
+  Q_set :: "int set" where
   "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
   
-  S :: "(int * int) set"
+definition
+  S :: "(int * int) set" where
   "S = P_set <*> Q_set"
 
-  S1 :: "(int * int) set"
+definition
+  S1 :: "(int * int) set" where
   "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
 
-  S2 :: "(int * int) set"
+definition
+  S2 :: "(int * int) set" where
   "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
 
-  f1 :: "int => (int * int) set"
+definition
+  f1 :: "int => (int * int) set" where
   "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
 
-  f2 :: "int => (int * int) set"
+definition
+  f2 :: "int => (int * int) set" where
   "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
 
 lemma p_fact: "0 < (p - 1) div 2"