src/HOL/Old_Number_Theory/Legacy_GCD.thy
changeset 61762 d50b993b4fb9
parent 61382 efac889fccbc
child 61945 1135b8de26c3
     1.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Mon Nov 30 14:24:51 2015 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Dec 01 14:09:10 2015 +0000
     1.3 @@ -665,7 +665,8 @@
     1.4    apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
     1.5    apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
     1.6    apply (frule_tac a = m in pos_mod_bound)
     1.7 -  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
     1.8 +  apply (simp del: pos_mod_bound add: algebra_simps nat_diff_distrib gcd_diff2 nat_le_eq_zle)
     1.9 +  apply (metis dual_order.strict_implies_order gcd.simps gcd_0_left gcd_diff2 mod_by_0 nat_mono)
    1.10    done
    1.11  
    1.12  lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"