NEWS
changeset 13735 7de9342aca7a
parent 13648 610cedff5538
child 13745 a31e04831dd1
--- a/NEWS	Wed Nov 27 17:25:41 2002 +0100
+++ b/NEWS	Thu Nov 28 10:50:42 2002 +0100
@@ -6,6 +6,9 @@
 
 *** General ***
 
+* Provers/linorder: New generic prover for transitivity reasoning over
+linear orders.  Note: this prover is not efficient!
+
 * Provers/simplifier:
 
   - Completely reimplemented Asm_full_simp_tac:
@@ -87,6 +90,10 @@
 
 *** HOL ***
 
+* New tactic "trans_tac" and method "trans" instantiate
+Provers/linorder.ML for axclasses "order" and "linorder" (predicates
+"<=", "<" and "="). 
+
 * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main 
 HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";