--- 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";