author | nipkow |

Mon Sep 13 09:57:25 2004 +0200 (2004-09-13) | |

changeset 15200 | 09489fe6989f |

parent 15199 | 29ca1fe63e7b |

child 15201 | d73f9d49d835 |

*** empty log message ***

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.