# HG changeset patch
# User wenzelm
# Date 962474040 -7200
# Node ID a7c6ea7e57deb861e344587203083b4c7f54ed2d
# Parent  672b03038110970070a7f8f26e954901f0800bd5
* Isar/HOL/Calculation: new rules for substitution in inequalities
(monotonicity conditions are extracted to be proven terminally);

diff -r 672b03038110 -r a7c6ea7e57de NEWS
--- 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 ? / ??;