src/HOL/NumberTheory/Quadratic_Reciprocity.thy

   assumes q_g_2: "2 < q"
   assumes p_neq_q:      "p \<noteq> q"
 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"
 proof -
   from p_g_2 have "2 \<le> p - 1" by arith