add HOL4
authorkleing
Mon Apr 19 08:20:52 2004 +0200 (2004-04-19)
changeset 146249b3397a848c3
parent 14623 811c09d426cc
child 14625 1ef710003a35
add HOL4
ANNOUNCE
Admin/page/main-content/index.content
NEWS
     1.1 --- a/ANNOUNCE	Mon Apr 19 00:45:50 2004 +0200
     1.2 +++ b/ANNOUNCE	Mon Apr 19 08:20:52 2004 +0200
     1.3 @@ -8,6 +8,9 @@
     1.4  (see the NEWS of the distribution for more details):
     1.5  
     1.6  
     1.7 +* New image HOL4 with imported library from HOL4 system on top of
     1.8 +  HOL-Complex (about 2500 additional theorems). 
     1.9 +
    1.10  * New theory Ring_and_Field with over 250 basic numerical laws, 
    1.11    all proved in axiomatic type classes for semirings, rings and fields.
    1.12  
     2.1 --- a/Admin/page/main-content/index.content	Mon Apr 19 00:45:50 2004 +0200
     2.2 +++ b/Admin/page/main-content/index.content	Mon Apr 19 08:20:52 2004 +0200
     2.3 @@ -38,6 +38,9 @@
     2.4  <h2><!-- _GP_ distname --></h2>
     2.5  New features in <strong><!-- _GP_ distname --></strong> include
     2.6  <ul>
     2.7 +<li>New image HOL4 with imported library from HOL4 system on top of
     2.8 +  HOL-Complex (about 2500 additional theorems).</li>
     2.9 +
    2.10  <li>New theory Ring_and_Field with over 250 basic numerical laws, 
    2.11    all proved in axiomatic type classes for semirings, rings and fields.</li>
    2.12  
     3.1 --- a/NEWS	Mon Apr 19 00:45:50 2004 +0200
     3.2 +++ b/NEWS	Mon Apr 19 08:20:52 2004 +0200
     3.3 @@ -100,6 +100,12 @@
     3.4  
     3.5  *** HOL ***
     3.6  
     3.7 +* Proof import: new image HOL4 contains the imported library from
     3.8 +  the HOL4 system with about 2500 theorems. It is imported by
     3.9 +  replaying proof terms produced by HOL4 in Isabelle. The HOL4 image
    3.10 +  can be used like any other Isabelle image.  See
    3.11 +  HOL/Import/HOL/README for more information.
    3.12 +
    3.13  * Simplifier:
    3.14    - Much improved handling of linear and partial orders.
    3.15      Reasoners for linear and partial orders are set up for type classes