# HG changeset patch
# User haftmann
# Date 1214893140 -7200
# Node ID 594fd97ce3d1c1fd381e27fb44b6106aecadf45b
# Parent  b8ff8497de6aa48fce0b092c563e280b2dfe4fb4
HOL += HOL-Complex

diff -r b8ff8497de6a -r 594fd97ce3d1 NEWS
--- a/NEWS	Tue Jul 01 08:05:08 2008 +0200
+++ b/NEWS	Tue Jul 01 08:19:00 2008 +0200
@@ -28,7 +28,11 @@
 
 *** HOL ***
 
-* Integrated image HOL-Complex with HOL.
+* Integrated image HOL-Complex with HOL.  Entry points Main.thy and
+Complex_Main.thy remain as they are.
+
+* New image HOL-Plain provides a minimal HOL with the most important tools
+available (inductive, datatype, primrec, codegen, ...).
 
 * Methods "case_tac" and "induct_tac" now refer to the very same rules
 as the structured Isar versions "cases" and "induct", cf. the