src/Doc/Corec/Corec.thy
changeset 67051 e7e54a0b9197
parent 66453 cc19f7ca2ed6
child 67399 eab6ce8368fa
     1.1 --- a/src/Doc/Corec/Corec.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/Doc/Corec/Corec.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -334,9 +334,9 @@
     1.4            primes m (n + 1))"
     1.5        apply (relation "measure (\<lambda>(m, n).
     1.6          if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
     1.7 -       apply (auto simp: mod_Suc intro: Suc_lessI)
     1.8 -       apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
     1.9 -      by (metis diff_less_mono2 lessI mod_less_divisor)
    1.10 +       apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE)
    1.11 +      apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel)
    1.12 +      done
    1.13  
    1.14  text \<open>
    1.15  \noindent