# HG changeset patch
# User wenzelm
# Date 918764721 -3600
# Node ID 37b76155a49e0e9d0c73c9cecfd7a51ad2aad7b8
# Parent  6e64b1cc76f80708395cf40e4181b034cb837b3f
Symbol.output subject to print mode;

diff -r 6e64b1cc76f8 -r 37b76155a49e NEWS
--- a/NEWS	Thu Feb 11 21:19:56 1999 +0100
+++ b/NEWS	Thu Feb 11 21:25:21 1999 +0100
@@ -58,6 +58,11 @@
 NB: At the moment, these decision procedures do not cope with mixed nat/int
 formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'.
 
+* HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
+-- avoids syntactic ambiguities and treats state, transition, and
+temporal levels more uniformly; introduces INCOMPATIBILITIES due to
+changed syntax and (many) tactics;
+
 
 *** Internal programming interfaces ***
 
@@ -69,10 +74,9 @@
 uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
 string -> unit if you really want to output text without newline;
 
-* HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
--- avoids syntactic ambiguities and treats state, transition, and
-temporal levels more uniformly; introduces INCOMPATIBILITIES due to
-changed syntax and (many) tactics;
+* Symbol.output subject to print mode; INCOMPATIBILITY: defaults to
+plain output, interface builders may have to enable 'isabelle_font'
+mode to get Isabelle font glyphs as before;
 
 
 *** ZF ***