NEWS
changeset 14854 61bdf2ae4dc5
parent 14816 b77cebcd7e6e
child 14878 b884a7ba7238
--- a/NEWS	Tue Jun 01 11:25:26 2004 +0200
+++ b/NEWS	Tue Jun 01 12:33:50 2004 +0200
@@ -32,6 +32,11 @@
   instead of 'nonterminals'/'syntax'.  Some very exotic syntax
   specifications may require further adaption (e.g. Cube/Base.thy).
 
+* Pure: removed obsolete type class "logic", use the top sort {}
+  instead.  Note that non-logical types should be declared as
+  'nonterminals' rather than 'types'.  INCOMPATIBILITY for new
+  object-logic specifications.
+
 * Pure/Syntax: inner syntax includes (*(*nested*) comments*).
 
 * Pure/Syntax: pretty pinter now supports unbreakable blocks,