# HG changeset patch
# User nipkow
# Date 1095062245 -7200
# Node ID 09489fe6989f5469b3318acc910aad92765d15d1
# Parent  29ca1fe63e7b08f70a41ea64db02f9964ff9f8f8
*** empty log message ***

diff -r 29ca1fe63e7b -r 09489fe6989f NEWS
--- a/NEWS	Sat Sep 11 18:35:43 2004 +0200
+++ b/NEWS	Mon Sep 13 09:57:25 2004 +0200
@@ -212,11 +212,16 @@
   Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e'
   now translates into 'setsum' as above.
 
-* HOL/Simplifier: Is now set up to reason about transitivity chains
-  involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics
-  provided by Provers/trancl.ML as additional solvers.
-  INCOMPATIBILITY: old proofs break occasionally as simplification may
-  now solve more goals than previously.
+* HOL/Simplifier:
+
+  - Is now set up to reason about transitivity chains involving "trancl"
+  (r^+) and "rtrancl" (r^*) by setting up tactics provided by
+  Provers/trancl.ML as additional solvers.  INCOMPATIBILITY: old proofs break
+  occasionally as simplification may now solve more goals than previously.
+
+  - Converts x <= y into x = y if assumption y <= x is present.  Works for
+  all partial orders (class "order"), in particular numbers and sets. For
+  linear orders (e.g. numbers) it treats ~ x < y just like y <= x.
 
 * HOL: new 'isatool dimacs2hol' to convert files in DIMACS CNF format
   (containing Boolean satisfiability problems) into Isabelle/HOL theories.