# HG changeset patch
# User kleing
# Date 1082355652 -7200
# Node ID 9b3397a848c3f6379bc1547817989e42483627b4
# Parent  811c09d426ccf53ebf9a8004d97a99b36b11b042
add HOL4

diff -r 811c09d426cc -r 9b3397a848c3 ANNOUNCE
--- 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.
 
diff -r 811c09d426cc -r 9b3397a848c3 Admin/page/main-content/index.content
--- 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>
 
diff -r 811c09d426cc -r 9b3397a848c3 NEWS
--- 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