dropped duplicates
authorhaftmann
Sun Oct 08 22:28:21 2017 +0200 (19 months ago)
changeset 66811aa288270732a
parent 66810 cc2b490f9dc4
child 66812 7163b780549d
dropped duplicates
src/HOL/Tools/nat_numeral_simprocs.ML
     1.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -41,17 +41,9 @@
     1.4           handle TERM _ => find_first_numeral (t::past) terms)
     1.5    | find_first_numeral past [] = raise TERM("find_first_numeral", []);
     1.6  
     1.7 -val zero = mk_number 0;
     1.8 -val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
     1.9 +val mk_sum = Arith_Data.mk_sum HOLogic.natT;
    1.10  
    1.11 -(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
    1.12 -fun mk_sum []        = zero
    1.13 -  | mk_sum [t,u]     = mk_plus (t, u)
    1.14 -  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.15 -
    1.16 -(*this version ALWAYS includes a trailing zero*)
    1.17 -fun long_mk_sum []        = HOLogic.zero
    1.18 -  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.19 +val long_mk_sum = Arith_Data.long_mk_sum HOLogic.natT;
    1.20  
    1.21  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
    1.22