src/HOL/Integ/NatSimprocs.thy
changeset 14378 69c4d5997669
parent 14353 79f9fbef9106
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Integ/NatSimprocs.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  (*Now just instantiating n to (number_of v) does the right simplification,
     1.5    but with some redundant inequality tests.*)
     1.6  lemma neg_number_of_bin_pred_iff_0:
     1.7 -     "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"
     1.8 +     "neg (number_of (bin_pred v)::int) = (number_of v = (0::nat))"
     1.9  apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ")
    1.10  apply (simp only: less_Suc_eq_le le_0_eq)
    1.11  apply (subst less_number_of_Suc, simp)
    1.12 @@ -29,7 +29,7 @@
    1.13  text{*No longer required as a simprule because of the @{text inverse_fold}
    1.14     simproc*}
    1.15  lemma Suc_diff_number_of:
    1.16 -     "neg (number_of (bin_minus v)) ==>  
    1.17 +     "neg (number_of (bin_minus v)::int) ==>  
    1.18        Suc m - (number_of v) = m - (number_of (bin_pred v))"
    1.19  apply (subst Suc_diff_eq_diff_pred, simp, simp)
    1.20  apply (force simp only: diff_nat_number_of less_0_number_of [symmetric]