diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/ex/BinEx.thy
--- a/src/HOL/ex/BinEx.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/ex/BinEx.thy	Thu May 30 10:12:52 2002 +0200
@@ -342,18 +342,35 @@
   apply (erule normal.induct)
      apply auto
   done
-
+(*
 lemma bin_minus_normal: "w \<in> normal ==> bin_minus w \<in> normal"
   apply (erule normal.induct)
      apply (simp_all add: bin_minus_BIT)
   apply (rule normal.intros)
-  apply assumption
+   apply assumption
   apply (simp add: normal_Pls_eq_0)
   apply (simp only: number_of_minus iszero_def zminus_equation [of _ "0"])
+
+The previous command should have finished the proof but the lin-arith
+procedure at the end of simplificatioon fails.
+Problem: lin-arith correctly derives the contradictory thm
+"number_of w + 1 + - 0 \<le> 0 + number_of w"  [..]
+which its local simplification setup should turn into False.
+But on the way we get
+
+Procedure "int_add_eval_numerals" produced rewrite rule:
+number_of ?v3 + 1 \<equiv> number_of (bin_add ?v3 (Pls BIT True))
+
+and eventually we arrive not at false but at
+
+"\<not> neg (number_of (bin_add w (bin_minus (bin_add w (Pls BIT True)))))"
+
+The next 2 commands should now be obsolete:
   apply (rule not_sym)
   apply simp
   done
 
+needs the previous thm:
 lemma bin_mult_normal [rule_format]:
     "w \<in> normal ==> z \<in> normal --> bin_mult w z \<in> normal"
   apply (erule normal.induct)
@@ -361,5 +378,5 @@
   apply (safe dest!: normal_BIT_D)
   apply (simp add: bin_add_normal)
   done
-
+*)
 end