1.1 --- a/src/HOL/Number_Theory/Residues.thy	Tue Mar 10 11:56:32 2015 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Tue Mar 10 15:20:40 2015 +0000
     1.3 @@ -8,10 +8,7 @@
     1.4  section {* Residue rings *}
     1.5  
     1.6  theory Residues
     1.7 -imports
     1.8 -  UniqueFactorization
     1.9 -  Binomial
    1.10 -  MiscAlgebra
    1.11 +imports UniqueFactorization MiscAlgebra
    1.12  begin
    1.13  
    1.14  (*
    1.15 @@ -275,15 +272,15 @@
    1.16    then have cop: "\<And>x. x \<in> {1::nat..p - 1} \<Longrightarrow> coprime x p"
    1.17      by blast
    1.18    { fix x::nat assume *: "1 < x" "x < p" and "x dvd p"
    1.19 -    have "coprime x p" 
    1.20 +    have "coprime x p"
    1.21        apply (rule cop)
    1.22        using * apply auto
    1.23        done
    1.24      with `x dvd p` `1 < x` have "False" by auto }
    1.25 -  then show ?thesis 
    1.26 -    using `2 \<le> p` 
    1.27 +  then show ?thesis
    1.28 +    using `2 \<le> p`
    1.29      by (simp add: prime_def)
    1.30 -       (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 
    1.31 +       (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
    1.32                not_numeral_le_zero one_dvd)
    1.33  qed
    1.34  
    1.35 @@ -367,7 +364,7 @@
    1.36    also have "phi p = nat p - 1"
    1.37      by (rule phi_prime, rule assms)
    1.38    finally show ?thesis
    1.39 -    by (metis nat_int) 
    1.40 +    by (metis nat_int)
    1.41  qed
    1.42  
    1.43  lemma fermat_theorem_nat:
    1.44 @@ -441,7 +438,7 @@
    1.45  lemma wilson_theorem:
    1.46    assumes "prime p" shows "[fact (p - 1) = - 1] (mod p)"
    1.47  proof (cases "p = 2")
    1.48 -  case True 
    1.49 +  case True
    1.50    then show ?thesis
    1.51      by (simp add: cong_int_def fact_altdef_nat)
    1.52  next