# HG changeset patch
# User paulson
# Date 1066293126 -7200
# Node ID a486123e24a5edb8e14de5d2d7c0ed6680445793
# Parent  c73d62ce9d1ce494462ed37f4031160f449f14ad
line-breaks; rewording

diff -r c73d62ce9d1c -r a486123e24a5 NEWS
--- a/NEWS	Thu Oct 16 10:31:40 2003 +0200
+++ b/NEWS	Thu Oct 16 10:32:06 2003 +0200
@@ -17,15 +17,17 @@
   symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
   existing theory and ML files.
 
+* Pure: Macintosh and Windows line-breaks are now allowed in theory files.
+
 * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 
   allowed in identifiers. Similar to greek letters \<^isub> is now considered 
   a normal (but invisible) letter. For multiple letter subscripts repeat 
   \<^isub> like this: x\<^isub>1\<^isub>2. 
 
-* Pure: Using the functions Theory.add_finals or Theory.add_finals_i
-  or the new Isar command "finalconsts", it is now possible to
-  make constants "final", thereby ensuring that they are not defined
-  later.  Useful for constants whose behaviour is fixed axiomatically
+* Pure: Using new Isar command "finalconsts" (or the ML functions
+  Theory.add_finals or Theory.add_finals_i) it is now possible to
+  declare constants "final", which prevents their being given a definition
+  later.  It is useful for constants whose behaviour is fixed axiomatically
   rather than definitionally, such as the meta-logic connectives.
 
 *** Isar ***