--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed Aug 30 03:19:08 2006 +0200
@@ -193,8 +193,6 @@
then show ?thesis by auto
qed
-ML {* fast_arith_split_limit := 0; *} (*FIXME*)
-
lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
(p * b \<noteq> q * a)"
proof
@@ -236,8 +234,6 @@
with q_g_2 show False by auto
qed
-ML {* fast_arith_split_limit := 9; *} (*FIXME*)
-
lemma (in QRTEMP) P_set_finite: "finite (P_set)"
using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)