--- a/ANNOUNCE Mon Apr 19 00:45:50 2004 +0200
+++ b/ANNOUNCE Mon Apr 19 08:20:52 2004 +0200
@@ -8,6 +8,9 @@
(see the NEWS of the distribution for more details):
+* New image HOL4 with imported library from HOL4 system on top of
+ HOL-Complex (about 2500 additional theorems).
+
* New theory Ring_and_Field with over 250 basic numerical laws,
all proved in axiomatic type classes for semirings, rings and fields.
--- a/Admin/page/main-content/index.content Mon Apr 19 00:45:50 2004 +0200
+++ b/Admin/page/main-content/index.content Mon Apr 19 08:20:52 2004 +0200
@@ -38,6 +38,9 @@
<h2><!-- _GP_ distname --></h2>
New features in <strong><!-- _GP_ distname --></strong> include
<ul>
+<li>New image HOL4 with imported library from HOL4 system on top of
+ HOL-Complex (about 2500 additional theorems).</li>
+
<li>New theory Ring_and_Field with over 250 basic numerical laws,
all proved in axiomatic type classes for semirings, rings and fields.</li>
--- a/NEWS Mon Apr 19 00:45:50 2004 +0200
+++ b/NEWS Mon Apr 19 08:20:52 2004 +0200
@@ -100,6 +100,12 @@
*** HOL ***
+* Proof import: new image HOL4 contains the imported library from
+ the HOL4 system with about 2500 theorems. It is imported by
+ replaying proof terms produced by HOL4 in Isabelle. The HOL4 image
+ can be used like any other Isabelle image. See
+ HOL/Import/HOL/README for more information.
+
* Simplifier:
- Much improved handling of linear and partial orders.
Reasoners for linear and partial orders are set up for type classes