*** empty log message ***
authornipkow
Mon Sep 13 09:57:25 2004 +0200 (2004-09-13)
changeset 1520009489fe6989f
parent 15199 29ca1fe63e7b
child 15201 d73f9d49d835
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Sat Sep 11 18:35:43 2004 +0200
     1.2 +++ b/NEWS	Mon Sep 13 09:57:25 2004 +0200
     1.3 @@ -212,11 +212,16 @@
     1.4    Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e'
     1.5    now translates into 'setsum' as above.
     1.6  
     1.7 -* HOL/Simplifier: Is now set up to reason about transitivity chains
     1.8 -  involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics
     1.9 -  provided by Provers/trancl.ML as additional solvers.
    1.10 -  INCOMPATIBILITY: old proofs break occasionally as simplification may
    1.11 -  now solve more goals than previously.
    1.12 +* HOL/Simplifier:
    1.13 +
    1.14 +  - Is now set up to reason about transitivity chains involving "trancl"
    1.15 +  (r^+) and "rtrancl" (r^*) by setting up tactics provided by
    1.16 +  Provers/trancl.ML as additional solvers.  INCOMPATIBILITY: old proofs break
    1.17 +  occasionally as simplification may now solve more goals than previously.
    1.18 +
    1.19 +  - Converts x <= y into x = y if assumption y <= x is present.  Works for
    1.20 +  all partial orders (class "order"), in particular numbers and sets. For
    1.21 +  linear orders (e.g. numbers) it treats ~ x < y just like y <= x.
    1.22  
    1.23  * HOL: new 'isatool dimacs2hol' to convert files in DIMACS CNF format
    1.24    (containing Boolean satisfiability problems) into Isabelle/HOL theories.