src/HOL/Divides.thy
changeset 35216 7641e8d831d2
parent 35050 9f841f20dca6
child 35367 45a193f0ed0c
     1.1 --- a/src/HOL/Divides.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/Divides.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -1090,7 +1090,7 @@
     1.4  lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
     1.5  apply (subgoal_tac "m mod 2 < 2")
     1.6  apply (erule less_2_cases [THEN disjE])
     1.7 -apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
     1.8 +apply (simp_all (no_asm_simp) add: Let_def mod_Suc)
     1.9  done
    1.10  
    1.11  lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
    1.12 @@ -1929,7 +1929,7 @@
    1.13  apply (rule order_le_less_trans)
    1.14   apply (erule_tac [2] mult_strict_right_mono)
    1.15   apply (rule mult_left_mono_neg)
    1.16 -  using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps pos_mod_bound)
    1.17 +  using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)
    1.18   apply (simp)
    1.19  apply (simp)
    1.20  done
    1.21 @@ -1954,7 +1954,7 @@
    1.22   apply (erule mult_strict_right_mono)
    1.23   apply (rule_tac [2] mult_left_mono)
    1.24    apply simp
    1.25 - using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps pos_mod_bound)
    1.26 + using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)
    1.27  apply simp
    1.28  done
    1.29