diff -r f30b73385060 -r 25b068a99d2b src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -88,12 +88,11 @@
 
 text{*Suggested by Matthias Daum*}
 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
-apply (subgoal_tac "nat x div nat k < nat x") 
- apply (simp add: nat_div_distrib [symmetric])
+apply (subgoal_tac "nat x div nat k < nat x")
+ apply (simp (asm_lr) add: nat_div_distrib [symmetric])
 apply (rule Divides.div_less_dividend, simp_all) 
 done
 
-
 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
 
 (*"neg" is used in rewrite rules for binary comparisons*)
@@ -148,7 +147,6 @@
          else let d = z-z' in     
               if neg d then 0 else nat d)"
 apply (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
-apply (simp add: diff_is_0_eq nat_le_eq_zle)
 done
 
 lemma diff_nat_number_of [simp]: 
@@ -628,7 +626,6 @@
 
 lemma nat_number_of_Min: "number_of Numeral.Min = (0::nat)"
   apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
-  apply (simp add: neg_nat)
   done
 
 lemma nat_number_of_BIT_1:
@@ -676,7 +673,7 @@
 by (simp only: mult_2 nat_add_distrib of_nat_add) 
 
 lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
-by (simp only:  nat_number_of_def, simp)
+by (simp only: nat_number_of_def)
 
 lemma of_nat_number_of_lemma:
      "of_nat (number_of v :: nat) =