# HG changeset patch
# User wenzelm
# Date 877705605 -7200
# Node ID 173fcf95412f4999de5781c8f257868192db70e3
# Parent  8fc76a4876164940ee240266e02def4ed758bb6b
tuned;

diff -r 8fc76a487616 -r 173fcf95412f NEWS
--- a/NEWS	Fri Oct 24 11:56:12 1997 +0200
+++ b/NEWS	Fri Oct 24 17:06:45 1997 +0200
@@ -12,7 +12,7 @@
 old input syntactically incorrect (e.g. "%x.x"); isatool fixdots
 ensures space after dots (e.g. "%x. x"); set long_names for fully
 qualified output names; NOTE: in case of severe problems with backward
-campatibility try settin 'global_names' at compile time to disable
+campatibility try setting 'global_names' at compile time to disable
 qualified names for theories; may also fine tune theories via 'global'
 and 'local' section;
 
@@ -71,7 +71,7 @@
 
 *** Syntax ***
 
-* no longer handles consts with name "" -- use syntax instead;
+* no longer handles consts with name "" -- declare as 'syntax' instead;
 
 * pretty printer: changed order of mixfix annotation preference (again!);
 
@@ -80,6 +80,12 @@
 
 *** HOL ***
 
+* HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of
+Actions;
+
+* HOL/Auth: new protocol proofs including some for the Internet
+protocol TLS;
+
 * HOL/Map: new theory of `maps' a la VDM.
 
 * HOL/simplifier: added infix function `addsplits':
@@ -94,14 +100,10 @@
 * HOL/Lists: the function "set_of_list" has been renamed "set" (and
 its theorems too);
 
-* HOL/Auth: new protocol proofs including some for the Internet protocol TLS
-
-* HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions
-
 
 *** HOLCF ***
 
-* HOLCF: fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
+* HOLCF: fixed LAM <x,y,zs>.b syntax;
 
 * added extended adm_tac to simplifier in HOLCF -- can now discharge
 adm (%x. P (t x)), where P is chainfinite and t continuous;