src/HOL/Number_Theory/Residues.thy
 changeset 59667 651ea265d568 parent 58889 5b7a9633cfa8 child 59730 b7c394c7a619
```     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
```