# HG changeset patch
# User haftmann
# Date 1179834930 -7200
# Node ID bf058e6405f88d8c0ae4ae8eac33ea04c96986b7
# Parent  c5b896d9788c40e0395f140907f1c7ef9b351a94
adjusted to change in Provers/Arith/combine_numerals.ML

diff -r c5b896d9788c -r bf058e6405f8 src/ZF/Integ/int_arith.ML
--- a/src/ZF/Integ/int_arith.ML	Tue May 22 13:40:37 2007 +0200
+++ b/src/ZF/Integ/int_arith.ML	Tue May 22 13:55:30 2007 +0200
@@ -1,6 +1,6 @@
 (*  Title:      ZF/Integ/int_arith.ML
     ID:         $Id$
-    Author:    Larry Paulson
+    Author:     Larry Paulson
     Copyright   2000  University of Cambridge
 
 Simprocs for linear arithmetic.
@@ -293,6 +293,8 @@
 
 structure CombineNumeralsData =
   struct
+  type coeff            = IntInf.int
+  val iszero            = (fn x => x = 0)
   val add               = IntInf.+ 
   val mk_sum            = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
   val dest_sum          = dest_sum
@@ -331,6 +333,8 @@
 
 structure CombineNumeralsProdData =
   struct
+  type coeff            = IntInf.int
+  val iszero            = (fn x => x = 0)
   val add               = IntInf.*
   val mk_sum            = (fn T:typ => mk_prod)
   val dest_sum          = dest_prod
@@ -341,7 +345,9 @@
   val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
   fun trans_tac _       = ArithData.gen_trans_tac trans
 
-  val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
+
+
+val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
   val norm_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym] @
     bin_simps @ zmult_ac @ tc_rules @ intifys
   fun norm_tac ss =