tuned;

--- a/src/HOL/NumberTheory/Gauss.thy	Fri Nov 10 10:42:25 2006 +0100
+++ b/src/HOL/NumberTheory/Gauss.thy	Fri Nov 10 10:42:28 2006 +0100
@@ -59,9 +59,8 @@
 lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
   using zdiv_zmult_self2 [of 2 "p - 1"] by auto
 
-end
 
-lemma zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
+lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
   apply (frule odd_minus_one_even)
   apply (simp add: zEven_def)
   apply (subgoal_tac "2 \<noteq> 0")
@@ -69,8 +68,6 @@
   apply (auto simp add: even_div_2_prop2)
   done
 
-context GAUSS
-begin
 
 lemma p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
   apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)

--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Fri Nov 10 10:42:25 2006 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Fri Nov 10 10:42:28 2006 +0100
@@ -371,9 +371,7 @@
   ultimately show ?thesis ..
 qed
 
-end
-
-lemma aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
+lemma (in -) aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
              (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
 proof-
   assume "zprime p" and "zprime q" and "2 < p" and "2 < q"
@@ -402,9 +400,6 @@
     using prems by auto
 qed
 
-context QRTEMP
-begin
-
 lemma aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
 proof
   fix j
@@ -582,17 +577,14 @@
   finally show ?thesis .
 qed
 
-end
 
-lemma pq_prime_neq: "[| zprime p; zprime q; p \<noteq> q |] ==> (~[p = 0] (mod q))"
+lemma (in -) pq_prime_neq: "[| zprime p; zprime q; p \<noteq> q |] ==> (~[p = 0] (mod q))"
   apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
   apply (drule_tac x = q in allE)
   apply (drule_tac x = p in allE)
   apply auto
   done
 
-context QRTEMP
-begin
 
 lemma QR_short: "(Legendre p q) * (Legendre q p) =
     (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"