src/HOL/Tools/nat_arith.ML
changeset 35092 cfe605c54e50
parent 35064 1bdef0c013d3
child 35267 8dfd816713c6
     1.1 --- a/src/HOL/Tools/nat_arith.ML	Wed Feb 10 14:12:02 2010 +0100
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Wed Feb 10 14:12:04 2010 +0100
     1.3 @@ -69,16 +69,16 @@
     1.4  structure LessCancelSums = CancelSumsFun
     1.5  (struct
     1.6    open CommonCancelSums;
     1.7 -  val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less};
     1.8 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT;
     1.9 +  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
    1.10 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
    1.11    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
    1.12  end);
    1.13  
    1.14  structure LeCancelSums = CancelSumsFun
    1.15  (struct
    1.16    open CommonCancelSums;
    1.17 -  val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq};
    1.18 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT;
    1.19 +  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
    1.20 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
    1.21    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
    1.22  end);
    1.23