src/HOL/Tools/nat_arith.ML
changeset 34974 18b41bba42b5
parent 32010 cb1a1c94b4cd
child 35047 1b2bae06c796
     1.1 --- a/src/HOL/Tools/nat_arith.ML	Thu Jan 28 11:48:43 2010 +0100
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Thu Jan 28 11:48:49 2010 +0100
     1.3 @@ -19,8 +19,8 @@
     1.4  
     1.5  (** abstract syntax of structure nat: 0, Suc, + **)
     1.6  
     1.7 -val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
     1.8 -val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
     1.9 +val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
    1.10 +val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT;
    1.11  
    1.12  fun mk_sum [] = HOLogic.zero
    1.13    | mk_sum [t] = t
    1.14 @@ -69,24 +69,24 @@
    1.15  structure LessCancelSums = CancelSumsFun
    1.16  (struct
    1.17    open CommonCancelSums;
    1.18 -  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
    1.19 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
    1.20 +  val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less};
    1.21 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT;
    1.22    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
    1.23  end);
    1.24  
    1.25  structure LeCancelSums = CancelSumsFun
    1.26  (struct
    1.27    open CommonCancelSums;
    1.28 -  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
    1.29 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
    1.30 +  val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq};
    1.31 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT;
    1.32    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
    1.33  end);
    1.34  
    1.35  structure DiffCancelSums = CancelSumsFun
    1.36  (struct
    1.37    open CommonCancelSums;
    1.38 -  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
    1.39 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
    1.40 +  val mk_bal = HOLogic.mk_binop @{const_name Algebras.minus};
    1.41 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT;
    1.42    val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
    1.43  end);
    1.44