--- a/src/HOL/NumberTheory/Gauss.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy Wed Jul 26 19:23:04 2006 +0200
@@ -104,8 +104,6 @@
apply (auto simp add: A_def ResSet_def)
apply (rule_tac m = p in zcong_less_eq)
apply (insert p_g_2, auto)
- apply (subgoal_tac [1-2] "(p - 1) div 2 < p")
- apply (auto, auto simp add: p_minus_one_l)
done
lemma (in GAUSS) B_res: "ResSet p B"
@@ -255,6 +253,8 @@
lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
by (auto simp add: D_eq)
+ML {* fast_arith_split_limit := 0; *} (*FIXME*)
+
lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
apply (auto simp add: F_eq A_def)
proof -
@@ -270,6 +270,8 @@
using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
qed
+ML {* fast_arith_split_limit := 9; *} (*FIXME*)
+
lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)