equal
deleted
inserted
replaced
86 (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1) |
86 (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1) |
87 in SOME thm end handle Cancel => NONE; |
87 in SOME thm end handle Cancel => NONE; |
88 |
88 |
89 val sum_conv = |
89 val sum_conv = |
90 Simplifier.mk_simproc "cancel_sums" |
90 Simplifier.mk_simproc "cancel_sums" |
91 (map (Drule.cterm_fun Logic.varify) Data.sum_pats) (K sum_proc); |
91 (map (Drule.cterm_fun Logic.varify_global) Data.sum_pats) (K sum_proc); |
92 |
92 |
93 |
93 |
94 (*A simproc to cancel like terms on the opposite sides of relations: |
94 (*A simproc to cancel like terms on the opposite sides of relations: |
95 (x + y - z < -z + x) = (y < 0) |
95 (x + y - z < -z + x) = (y < 0) |
96 Works for (=) and (<=) as well as (<), if the necessary rules are supplied. |
96 Works for (=) and (<=) as well as (<), if the necessary rules are supplied. |