| changeset 9229 | a7c6ea7e57de |
| parent 9224 | 0da360494917 |
| child 9239 | b31c2132176a |
--- a/NEWS Sat Jul 01 19:51:08 2000 +0200 +++ b/NEWS Sat Jul 01 19:54:00 2000 +0200 @@ -127,6 +127,9 @@ * HOL: removed 'case_split' thm binding, should use 'cases' proof method anyway; +* HOL/Calculation: new rules for substitution in inequalities +(monotonicity conditions are extracted to be proven terminally); + * names of theorems etc. may be natural numbers as well; * Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??;