--- a/NEWS Tue Sep 27 11:03:38 2005 +0200
+++ b/NEWS Tue Sep 27 11:27:07 2005 +0200
@@ -247,15 +247,13 @@
theory development.
* Code generator is now invoked via code_module (incremental code
- generation) and code_library (modular code generation, ML structures
- for each theory).
- INCOMPATIBILITY: new keywords "file" and "contains" must be quoted
- when used as identifier names.
-
-* New "value" command for parsing, evaluating and printing terms
- using the code generator.
- INCOMPATIBILITY: new keyword "value" must be quoted when used as
- identifier name.
+generation) and code_library (modular code generation, ML structures
+for each theory). INCOMPATIBILITY: new keywords 'file' and 'contains'
+must be quoted when used as identifiers.
+
+* New 'value' command for reading, evaluating and printing terms using
+the code generator. INCOMPATIBILITY: command keyword 'value' must be
+quoted when used as identifier.
*** Locales ***