src/HOL/Integ/int_factor_simprocs.ML
changeset 19277 f7602e74d948
parent 18442 b35d7312c64f
child 20044 92cc2f4c7335
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Thu Mar 16 20:19:25 2006 +0100
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Fri Mar 17 09:34:23 2006 +0100
     1.3 @@ -103,8 +103,8 @@
     1.4  structure LessCancelNumeralFactor = CancelNumeralFactorFun
     1.5   (open CancelNumeralFactorCommon
     1.6    val prove_conv = Bin_Simprocs.prove_conv
     1.7 -  val mk_bal   = HOLogic.mk_binrel "op <"
     1.8 -  val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
     1.9 +  val mk_bal   = HOLogic.mk_binrel "Orderings.less"
    1.10 +  val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
    1.11    val cancel = mult_less_cancel_left RS trans
    1.12    val neg_exchanges = true
    1.13  )
    1.14 @@ -112,8 +112,8 @@
    1.15  structure LeCancelNumeralFactor = CancelNumeralFactorFun
    1.16   (open CancelNumeralFactorCommon
    1.17    val prove_conv = Bin_Simprocs.prove_conv
    1.18 -  val mk_bal   = HOLogic.mk_binrel "op <="
    1.19 -  val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
    1.20 +  val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
    1.21 +  val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
    1.22    val cancel = mult_le_cancel_left RS trans
    1.23    val neg_exchanges = true
    1.24  )