changeset 40786 | 0a54cfc9add3 |
parent 38159 | e9b4835a54ee |
child 41541 | 1fa4725c4656 |
--- a/src/HOL/Old_Number_Theory/Euler.thy Sat Nov 27 17:44:36 2010 -0800 +++ b/src/HOL/Old_Number_Theory/Euler.thy Sun Nov 28 15:20:51 2010 +0100 @@ -94,7 +94,7 @@ subsection {* Properties of SetS *} lemma SetS_finite: "2 < p ==> finite (SetS a p)" - by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI) + by (auto simp add: SetS_def SRStar_finite [of p]) lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X" by (auto simp add: SetS_def MultInvPair_def)