src/HOL/Tools/nat_arith.ML
changeset 35092 cfe605c54e50
parent 35064 1bdef0c013d3
child 35267 8dfd816713c6
equal deleted inserted replaced
35091:59b41ba431b5 35092:cfe605c54e50
    67 end);
    67 end);
    68 
    68 
    69 structure LessCancelSums = CancelSumsFun
    69 structure LessCancelSums = CancelSumsFun
    70 (struct
    70 (struct
    71   open CommonCancelSums;
    71   open CommonCancelSums;
    72   val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less};
    72   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
    73   val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT;
    73   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
    74   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
    74   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
    75 end);
    75 end);
    76 
    76 
    77 structure LeCancelSums = CancelSumsFun
    77 structure LeCancelSums = CancelSumsFun
    78 (struct
    78 (struct
    79   open CommonCancelSums;
    79   open CommonCancelSums;
    80   val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq};
    80   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
    81   val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT;
    81   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
    82   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
    82   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
    83 end);
    83 end);
    84 
    84 
    85 structure DiffCancelSums = CancelSumsFun
    85 structure DiffCancelSums = CancelSumsFun
    86 (struct
    86 (struct