src/HOL/Divides.thy
changeset 66630 034cabc4fda5
parent 65556 fcd599570afa
child 66800 128e9ed9f63c
     1.1 --- a/src/HOL/Divides.thy	Fri Sep 08 00:02:31 2017 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri Sep 08 00:02:33 2017 +0200
     1.3 @@ -501,7 +501,7 @@
     1.4  
     1.5  lemma odd_iff_mod_2_eq_one:
     1.6    "odd a \<longleftrightarrow> a mod 2 = 1"
     1.7 -  by (auto simp add: even_iff_mod_2_eq_zero)
     1.8 +  by (simp add: even_iff_mod_2_eq_zero)
     1.9  
    1.10  lemma even_succ_div_two [simp]:
    1.11    "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
    1.12 @@ -1853,8 +1853,8 @@
    1.13    from assms have "sgn v = - 1 \<or> sgn v = 1"
    1.14      by (cases "v \<ge> 0") auto
    1.15    then show ?thesis
    1.16 -  using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
    1.17 -    by (auto simp add: not_less div_abs_eq_div_nat)
    1.18 +    using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
    1.19 +    by (fastforce simp add: not_less div_abs_eq_div_nat)
    1.20  qed
    1.21  
    1.22  lemma div_eq_sgn_abs:
    1.23 @@ -2031,7 +2031,7 @@
    1.24       "eucl_rel_int a b (q, r) ==> b \<noteq> 0
    1.25        ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
    1.26                            if r=0 then 0 else b-r)"
    1.27 -by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff right_diff_distrib)
    1.28 +by (force simp add: eucl_rel_int_iff right_diff_distrib)
    1.29  
    1.30  
    1.31  lemma zdiv_zminus1_eq_if: