--- a/src/HOL/Old_Number_Theory/Euler.thy Wed Mar 03 09:33:46 2010 +0100
+++ b/src/HOL/Old_Number_Theory/Euler.thy Wed Mar 03 10:48:19 2010 +0100
@@ -162,8 +162,11 @@
lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)"
by auto
+lemma d22set_induct_old: "(\<And>a::int. 1 < a \<longrightarrow> P (a - 1) \<Longrightarrow> P a) \<Longrightarrow> P x"
+using d22set.induct by blast
+
lemma SRStar_d22set_prop: "2 < p \<Longrightarrow> (SRStar p) = {1} \<union> (d22set (p - 1))"
- apply (induct p rule: d22set.induct)
+ apply (induct p rule: d22set_induct_old)
apply auto
apply (simp add: SRStar_def d22set.simps)
apply (simp add: SRStar_def d22set.simps, clarify)