changeset 14237 a486123e24a5
parent 14234 9590df3c5f2a
child 14243 0e2ec694784d
--- 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 ***