author haftmann Tue, 22 May 2007 13:55:30 +0200 changeset 23071 bf058e6405f8 parent 23070 c5b896d9788c child 23072 f64df9399329
adjusted to change in Provers/Arith/combine_numerals.ML
 src/ZF/Integ/int_arith.ML file | annotate | diff | comparison | revisions
```--- 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 =```