equal
deleted
inserted
replaced
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 |