adjusted to change in Provers/Arith/combine_numerals.ML
authorhaftmann
Tue May 22 13:55:30 2007 +0200 (2007-05-22)
changeset 23071bf058e6405f8
parent 23070 c5b896d9788c
child 23072 f64df9399329
adjusted to change in Provers/Arith/combine_numerals.ML
src/ZF/Integ/int_arith.ML
     1.1 --- a/src/ZF/Integ/int_arith.ML	Tue May 22 13:40:37 2007 +0200
     1.2 +++ b/src/ZF/Integ/int_arith.ML	Tue May 22 13:55:30 2007 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      ZF/Integ/int_arith.ML
     1.5      ID:         $Id$
     1.6 -    Author:    Larry Paulson
     1.7 +    Author:     Larry Paulson
     1.8      Copyright   2000  University of Cambridge
     1.9  
    1.10  Simprocs for linear arithmetic.
    1.11 @@ -293,6 +293,8 @@
    1.12  
    1.13  structure CombineNumeralsData =
    1.14    struct
    1.15 +  type coeff            = IntInf.int
    1.16 +  val iszero            = (fn x => x = 0)
    1.17    val add               = IntInf.+ 
    1.18    val mk_sum            = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
    1.19    val dest_sum          = dest_sum
    1.20 @@ -331,6 +333,8 @@
    1.21  
    1.22  structure CombineNumeralsProdData =
    1.23    struct
    1.24 +  type coeff            = IntInf.int
    1.25 +  val iszero            = (fn x => x = 0)
    1.26    val add               = IntInf.*
    1.27    val mk_sum            = (fn T:typ => mk_prod)
    1.28    val dest_sum          = dest_prod
    1.29 @@ -341,7 +345,9 @@
    1.30    val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
    1.31    fun trans_tac _       = ArithData.gen_trans_tac trans
    1.32  
    1.33 -  val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
    1.34 +
    1.35 +
    1.36 +val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
    1.37    val norm_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym] @
    1.38      bin_simps @ zmult_ac @ tc_rules @ intifys
    1.39    fun norm_tac ss =