# HG changeset patch
# User wenzelm
# Date 1085167738 -7200
# Node ID b702848de41fbc6d22bd3366120c44e79ce10185
# Parent  751d5af6d91e2fba9b4ca9df82a0df84e4231ae6
Pure: clear separation of logical types and nonterminals;

diff -r 751d5af6d91e -r b702848de41f NEWS
--- a/NEWS	Fri May 21 21:28:14 2004 +0200
+++ b/NEWS	Fri May 21 21:28:58 2004 +0200
@@ -33,6 +33,16 @@
 * Pure: tuned internal renaming of symbolic identifiers -- attach
   primes instead of base 26 numbers.
 
+* Pure: clear separation of logical types and nonterminals, where the
+  latter may only occur in 'syntax' specifications or type
+  abbreviations.  Before that distinction was only partially
+  implemented via type class "logic" vs. "{}".  Potential
+  INCOMPATIBILITY in rare cases of improper use of 'types'/'consts'
+  instead of 'nonterminals'/'syntax'.  Some very exotic syntax
+  specifications requiring additional non-logical non-syntactic types
+  (apart from 'prop' vs. 'logic') may need to be reformulated with
+  duplicated 'consts'/'syntax' declarations (e.g. see Cube/Base.thy).
+
 
 *** HOL ***