changeset 16733 | 236dfafbeb63 |
parent 16663 | 13e9c402308b |
child 16974 | 0f8ebabf3163 |
--- a/src/HOL/NumberTheory/Euler.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/NumberTheory/Euler.thy Thu Jul 07 12:39:17 2005 +0200 @@ -175,7 +175,7 @@ lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \<union> (d22set (p - 1))"; apply (induct p rule: d22set.induct, auto) - apply (simp add: SRStar_def d22set.simps, arith) + apply (simp add: SRStar_def d22set.simps) apply (simp add: SRStar_def d22set.simps, clarify) apply (frule aux1) apply (frule aux2, auto)