# HG changeset patch
# User wenzelm
# Date 1142350169 -3600
# Node ID efaf5d47049ebf8d85d352c085a326cf36d5ce4e
# Parent  f3ce97b5661aa032a10a6009e4c9f5b51f3fc18e
Pure: no_translations;

diff -r f3ce97b5661a -r efaf5d47049e NEWS
--- 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: