NEWS
changeset 14237 a486123e24a5
parent 14234 9590df3c5f2a
child 14243 0e2ec694784d
     1.1 --- a/NEWS	Thu Oct 16 10:31:40 2003 +0200
     1.2 +++ b/NEWS	Thu Oct 16 10:32:06 2003 +0200
     1.3 @@ -17,15 +17,17 @@
     1.4    symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
     1.5    existing theory and ML files.
     1.6  
     1.7 +* Pure: Macintosh and Windows line-breaks are now allowed in theory files.
     1.8 +
     1.9  * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 
    1.10    allowed in identifiers. Similar to greek letters \<^isub> is now considered 
    1.11    a normal (but invisible) letter. For multiple letter subscripts repeat 
    1.12    \<^isub> like this: x\<^isub>1\<^isub>2. 
    1.13  
    1.14 -* Pure: Using the functions Theory.add_finals or Theory.add_finals_i
    1.15 -  or the new Isar command "finalconsts", it is now possible to
    1.16 -  make constants "final", thereby ensuring that they are not defined
    1.17 -  later.  Useful for constants whose behaviour is fixed axiomatically
    1.18 +* Pure: Using new Isar command "finalconsts" (or the ML functions
    1.19 +  Theory.add_finals or Theory.add_finals_i) it is now possible to
    1.20 +  declare constants "final", which prevents their being given a definition
    1.21 +  later.  It is useful for constants whose behaviour is fixed axiomatically
    1.22    rather than definitionally, such as the meta-logic connectives.
    1.23  
    1.24  *** Isar ***