NEWS

 * ML: The exception LIST is no more, the standard exceptions Empty and
   Subscript, as well as Library.UnequalLengths are used instead.  This
   means that function like Library.hd and Library.tl are gone, as the
   standard hd and tl functions suffice.
 
-  A number of functions, specifically those in the LIBRARY_CLOSED
-  signature, are now no longer exported to the top ML level, as they
-  are variants of standard functions.  The following suggests how
-  one can translate existing code:
+  A number of basic functions are now no longer exported to the top ML
+  level, as they are variants of standard functions.  The following
+  suggests how one can translate existing code:
 
     the x = valOf x
     if_none x y = getOpt(x,y)
     is_some x = isSome x
     apsome f x = Option.map f x

 
 * 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: command 'no_syntax' removes grammar declarations (and
+  translations) resulting from the given syntax specification, which
+  is interpreted in the same manner as for the 'syntax' command.
 
 * Pure: print_tac now outputs the goal through the trace channel.
 
 * Pure: reference Namespace.unique_names included.  If true the
   (shortest) namespace-prefix is printed to disambiguate conflicts (as