src/HOL/Tools/nat_arith.ML
changeset 35267 8dfd816713c6
parent 35092 cfe605c54e50
child 38715 6513ea67d95d
     1.1 --- a/src/HOL/Tools/nat_arith.ML	Fri Feb 19 14:47:00 2010 +0100
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Fri Feb 19 14:47:01 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 Algebras.plus};
     1.8 -val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT;
     1.9 +val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    1.10 +val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
    1.11  
    1.12  fun mk_sum [] = HOLogic.zero
    1.13    | mk_sum [t] = t
    1.14 @@ -85,8 +85,8 @@
    1.15  structure DiffCancelSums = CancelSumsFun
    1.16  (struct
    1.17    open CommonCancelSums;
    1.18 -  val mk_bal = HOLogic.mk_binop @{const_name Algebras.minus};
    1.19 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT;
    1.20 +  val mk_bal = HOLogic.mk_binop @{const_name Groups.minus};
    1.21 +  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT;
    1.22    val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
    1.23  end);
    1.24