# HG changeset patch
# User huffman
# Date 1215179875 -7200
# Node ID a5de2cbf548ff03b84cef514141aa44028681502
# Parent  dbb9981c3d18486d4160db3d52e0e0a05e600dd2
HOL-NSA

diff -r dbb9981c3d18 -r a5de2cbf548f NEWS
--- a/NEWS	Fri Jul 04 07:39:01 2008 +0200
+++ b/NEWS	Fri Jul 04 15:57:55 2008 +0200
@@ -80,6 +80,14 @@
 theorems.  Changes in simp rules.  INCOMPATIBILITY.
 
 
+*** HOL-NSA ***
+
+* Created new image HOL-NSA, containing theories of nonstandard
+analysis which were previously part of HOL-Complex.  Entry point
+Hyperreal.thy remains valid, but theories formerly using
+Complex_Main.thy should now use new entry point Hypercomplex.thy.
+
+
 *** ML ***
  
 * Rules and tactics that read instantiations (read_instantiate,