--- a/NEWS Sat Apr 16 18:54:44 2005 +0200
+++ b/NEWS Sat Apr 16 18:55:28 2005 +0200
@@ -17,10 +17,9 @@
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)
@@ -108,6 +107,10 @@
'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