aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorAvi Shinnar2020-12-05 21:56:15 -0500
committerAvi Shinnar2020-12-09 08:40:11 -0500
commit29d2ffb5f5569efe8614efa30be560efc72a34f5 (patch)
tree64d49df94da5c5b2d4d5674d7caacf7b36c29822 /plugins
parent9e0ca704fa8273a8337ff9e118d2d08620af8962 (diff)
Redefines exp_ineq1 to hold for all non-zero numbers.
The original (which holds only for positive numbers) is now called exp_ineq1_pos. A version that holds only for negative numbers is added as exp_ineq1_neg. Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <). Co-authored-by: Barry M. Trager <bmt@us.ibm.com>
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions