src/HOL/GCD.thy
changeset 44278 1220ecb81e8f
parent 42871 1c0b99f950d9
child 44766 d4d33a4d7548
     1.1 --- a/src/HOL/GCD.thy	Thu Aug 18 13:25:17 2011 +0200
     1.2 +++ b/src/HOL/GCD.thy	Thu Aug 18 13:55:26 2011 +0200
     1.3 @@ -531,11 +531,8 @@
     1.4  
     1.5  lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
     1.6  apply(rule antisym)
     1.7 - apply(rule Max_le_iff[THEN iffD2])
     1.8 -   apply simp
     1.9 -  apply fastsimp
    1.10 - apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
    1.11 -apply simp
    1.12 + apply(rule Max_le_iff [THEN iffD2])
    1.13 +  apply (auto intro: abs_le_D1 dvd_imp_le_int)
    1.14  done
    1.15  
    1.16  lemma gcd_is_Max_divisors_nat: