# 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