diff -r bdf6b7adc3ec -r 0eca4aabf371 src/HOL/Integ/Bin.thy
--- a/src/HOL/Integ/Bin.thy	Fri Mar 19 11:06:53 2004 +0100
+++ b/src/HOL/Integ/Bin.thy	Wed Mar 24 10:50:29 2004 +0100
@@ -137,7 +137,7 @@
 lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
 proof (cases z rule: int_cases)
   case (nonneg n)
-  have le: "0 \<le> z+z" by (simp add: prems add_increasing) 
+  have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
   thus ?thesis using  le_imp_0_less [OF le]
     by (auto simp add: add_assoc) 
 next
@@ -147,7 +147,8 @@
     assume eq: "1 + z + z = 0"
     have "0 < 1 + (int n + int n)"
       by (simp add: le_imp_0_less add_increasing) 
-    also have "... = - (1 + z + z)" by (simp add: prems int_Suc add_ac) 
+    also have "... = - (1 + z + z)"
+      by (simp add: neg add_assoc [symmetric], simp add: add_commute) 
     also have "... = 0" by (simp add: eq) 
     finally have "0<0" ..
     thus False by blast
@@ -235,9 +236,9 @@
   assume "a \<in> range of_int"
   then obtain z where a: "a = of_int z" ..
   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
-    by (simp add: prems)
+    by (simp add: a)
   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
-  also have "... = (a < 0)" by (simp add: prems)
+  also have "... = (a < 0)" by (simp add: a)
   finally show ?thesis .
 qed