changeset 9571 | c869d1886a32 |
parent 9544 | f9202e219a29 |
child 10536 | 8f34ecae1446 |
--- a/src/HOL/Integ/nat_simprocs.ML Thu Aug 10 11:27:34 2000 +0200 +++ b/src/HOL/Integ/nat_simprocs.ML Thu Aug 10 11:30:22 2000 +0200 @@ -254,6 +254,7 @@ structure CombineNumeralsData = struct + val add = op + : int*int -> int val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *) val dest_sum = dest_Sucs_sum val mk_coeff = mk_coeff