NEWS
changeset 14624 9b3397a848c3
parent 14610 9c2e31e483b2
child 14655 8a95abf87dd3
     1.1 --- a/NEWS	Mon Apr 19 00:45:50 2004 +0200
     1.2 +++ b/NEWS	Mon Apr 19 08:20:52 2004 +0200
     1.3 @@ -100,6 +100,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Proof import: new image HOL4 contains the imported library from
     1.8 +  the HOL4 system with about 2500 theorems. It is imported by
     1.9 +  replaying proof terms produced by HOL4 in Isabelle. The HOL4 image
    1.10 +  can be used like any other Isabelle image.  See
    1.11 +  HOL/Import/HOL/README for more information.
    1.12 +
    1.13  * Simplifier:
    1.14    - Much improved handling of linear and partial orders.
    1.15      Reasoners for linear and partial orders are set up for type classes