src/HOL/Integ/Bin.ML

   by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); 
   by (ALLGOALS(int_case_tac "integ_of_bin w")); 
   by (ALLGOALS(asm_simp_tac 
                (simpset() addsimps[zminus_zadd_distrib RS sym, 
                                 znat_add RS sym]))); 
-  by (stac eq_False_conv 1); 
   by (rtac notI 1); 
   by (dres_inst_tac [("f","(% z. z +  $# Suc (Suc (n + n)))")] arg_cong 1); 
   by (Asm_full_simp_tac 1); 
 val iob_Bcons_eq_0 = result();