src/HOL/Integ/NatSimprocs.ML
changeset 11468 02cd5d5bc497
parent 11464 ddea204de5bc
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Integ/NatSimprocs.ML	Mon Aug 06 16:43:40 2001 +0200
     1.2 +++ b/src/HOL/Integ/NatSimprocs.ML	Tue Aug 07 16:36:52 2001 +0200
     1.3 @@ -14,15 +14,12 @@
     1.4  
     1.5  (*Now just instantiating n to (number_of v) does the right simplification,
     1.6    but with some redundant inequality tests.*)
     1.7 -(*
     1.8  Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))";
     1.9 -by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1);
    1.10 -by (Asm_simp_tac 1);
    1.11 +by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1')" 1);
    1.12 +by (asm_simp_tac (HOL_ss addsimps [less_Suc_eq_le, le_0_eq]) 1); 
    1.13  by (stac less_number_of_Suc 1);
    1.14  by (Simp_tac 1);
    1.15  qed "neg_number_of_bin_pred_iff_0";
    1.16 -*)
    1.17 -val neg_number_of_bin_pred_iff_0 = thm "neg_number_of_bin_pred_iff_0";
    1.18  
    1.19  Goal "neg (number_of (bin_minus v)) ==> \
    1.20  \     Suc m - (number_of v) = m - (number_of (bin_pred v))";