* Isar/HOL/Calculation: new rules for substitution in inequalities
(monotonicity conditions are extracted to be proven terminally);

--- 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 ? / ??;