# HG changeset patch # User paulson # Date 965900393 -7200 # Node ID da0a964aa601e6460d8a3ef65a38409b51f99aa2 # Parent 5cadc8146573de67e61505ef9f022c095cebd89f new structure field "add" for CombineNumerals diff -r 5cadc8146573 -r da0a964aa601 src/HOL/Real/RealBin.ML --- a/src/HOL/Real/RealBin.ML Thu Aug 10 11:33:40 2000 +0200 +++ b/src/HOL/Real/RealBin.ML Thu Aug 10 11:39:53 2000 +0200 @@ -457,6 +457,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_sum val mk_coeff = mk_coeff