src/HOL/Integ/NatSimprocs.ML
changeset 11464 ddea204de5bc
parent 11296 38a69e5d79fa
child 11468 02cd5d5bc497
     1.1 --- a/src/HOL/Integ/NatSimprocs.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Integ/NatSimprocs.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -14,13 +14,15 @@
     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 +(*
     1.9  Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))";
    1.10  by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1);
    1.11  by (Asm_simp_tac 1);
    1.12  by (stac less_number_of_Suc 1);
    1.13  by (Simp_tac 1);
    1.14  qed "neg_number_of_bin_pred_iff_0";
    1.15 +*)
    1.16 +val neg_number_of_bin_pred_iff_0 = thm "neg_number_of_bin_pred_iff_0";
    1.17  
    1.18  Goal "neg (number_of (bin_minus v)) ==> \
    1.19  \     Suc m - (number_of v) = m - (number_of (bin_pred v))";