1.1 --- a/NEWS	Wed Nov 27 17:25:41 2002 +0100
     1.2 +++ b/NEWS	Thu Nov 28 10:50:42 2002 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Provers/linorder: New generic prover for transitivity reasoning over
     1.8 +linear orders.  Note: this prover is not efficient!
     1.9 +
    1.10  * Provers/simplifier:
    1.11  
    1.12    - Completely reimplemented Asm_full_simp_tac:
    1.13 @@ -87,6 +90,10 @@
    1.14  
    1.15  *** HOL ***
    1.16  
    1.17 +* New tactic "trans_tac" and method "trans" instantiate
    1.18 +Provers/linorder.ML for axclasses "order" and "linorder" (predicates
    1.19 +"<=", "<" and "="). 
    1.20 +
    1.21  * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main 
    1.22  HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";
    1.23