NEWS
changeset 14795 b702848de41f
parent 14731 5670fc027a3b
child 14816 b77cebcd7e6e
     1.1 --- a/NEWS	Fri May 21 21:28:14 2004 +0200
     1.2 +++ b/NEWS	Fri May 21 21:28:58 2004 +0200
     1.3 @@ -33,6 +33,16 @@
     1.4  * Pure: tuned internal renaming of symbolic identifiers -- attach
     1.5    primes instead of base 26 numbers.
     1.6  
     1.7 +* Pure: clear separation of logical types and nonterminals, where the
     1.8 +  latter may only occur in 'syntax' specifications or type
     1.9 +  abbreviations.  Before that distinction was only partially
    1.10 +  implemented via type class "logic" vs. "{}".  Potential
    1.11 +  INCOMPATIBILITY in rare cases of improper use of 'types'/'consts'
    1.12 +  instead of 'nonterminals'/'syntax'.  Some very exotic syntax
    1.13 +  specifications requiring additional non-logical non-syntactic types
    1.14 +  (apart from 'prop' vs. 'logic') may need to be reformulated with
    1.15 +  duplicated 'consts'/'syntax' declarations (e.g. see Cube/Base.thy).
    1.16 +
    1.17  
    1.18  *** HOL ***
    1.19