--- a/NEWS Tue Mar 14 14:25:09 2006 +0100
+++ b/NEWS Tue Mar 14 16:29:29 2006 +0100
@@ -34,6 +34,9 @@
*** Pure ***
+* Command 'no_translations' removes translation rules from theory
+syntax.
+
* Isar: improper proof element 'guess' is like 'obtain', but derives
the obtained context from the course of reasoning! For example:
@@ -390,9 +393,10 @@
* Library: added theory Coinductive_List of potentially infinite lists
as greatest fixed-point.
-* Library: added theory AssocList which implements (finite) maps as
+* Library: added theory AssocList which implements (finite) maps as
association lists.
+
*** ML ***
* Pure/library: