1.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy	Sat Nov 27 17:44:36 2010 -0800
     1.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sun Nov 28 15:20:51 2010 +0100
     1.3 @@ -73,22 +73,22 @@
     1.4    done
     1.5  
     1.6  lemma finite_B: "finite (B)"
     1.7 -  by (auto simp add: B_def finite_A finite_imageI)
     1.8 +by (auto simp add: B_def finite_A)
     1.9  
    1.10  lemma finite_C: "finite (C)"
    1.11 -  by (auto simp add: C_def finite_B finite_imageI)
    1.12 +by (auto simp add: C_def finite_B)
    1.13  
    1.14  lemma finite_D: "finite (D)"
    1.15 -  by (auto simp add: D_def finite_Int finite_C)
    1.16 +by (auto simp add: D_def finite_Int finite_C)
    1.17  
    1.18  lemma finite_E: "finite (E)"
    1.19 -  by (auto simp add: E_def finite_Int finite_C)
    1.20 +by (auto simp add: E_def finite_Int finite_C)
    1.21  
    1.22  lemma finite_F: "finite (F)"
    1.23 -  by (auto simp add: F_def finite_E finite_imageI)
    1.24 +by (auto simp add: F_def finite_E)
    1.25  
    1.26  lemma C_eq: "C = D \<union> E"
    1.27 -  by (auto simp add: C_def D_def E_def)
    1.28 +by (auto simp add: C_def D_def E_def)
    1.29  
    1.30  lemma A_card_eq: "card A = nat ((p - 1) div 2)"
    1.31    apply (auto simp add: A_def)