src/HOL/Number_Theory/Residues.thy
changeset 55262 16724746ad89
parent 55261 ad3604df6bc6
child 55352 1d2852dfc4a7
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Sun Feb 02 21:48:28 2014 +0000
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Feb 03 00:22:48 2014 +0000
     1.3 @@ -312,9 +312,9 @@
     1.4        done
     1.5      with `x dvd p` `1 < x` have "False" by auto }
     1.6    then show ?thesis 
     1.7 -    using `2 \<le> p` apply (simp add: prime_def)
     1.8 -by (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 
     1.9 -  not_numeral_le_zero one_dvd)
    1.10 +    using `2 \<le> p` 
    1.11 +    by (simp add: prime_def)
    1.12 +       (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 not_numeral_le_zero one_dvd)
    1.13  qed
    1.14  
    1.15  lemma phi_zero [simp]: "phi 0 = 0"