# HG changeset patch
# User wenzelm
# Date 861701145 -7200
# Node ID 8a1eb4531fbb6fb3edbe2476befb64a470d49d0f
# Parent  645ec3d19ac1b369e463f6a03642157cee0113ba
tuned;

diff -r 645ec3d19ac1 -r 8a1eb4531fbb NEWS
--- a/NEWS	Mon Apr 21 13:49:40 1997 +0200
+++ b/NEWS	Tue Apr 22 11:25:45 1997 +0200
@@ -2,8 +2,8 @@
 Isabelle NEWS -- history of user-visible changes
 ================================================
 
-New in Isabelle94-8 (April 1997)
---------------------------------
+New in Isabelle94-8 (May 1997)
+------------------------------
 
 *** General Changes ***
 
@@ -12,12 +12,14 @@
 
 * INSTALL text, together with ./configure and ./build scripts;
 
-* reimplemented type inference for greater efficiency;
+* reimplemented type inference for greater efficiency, better error
+messages and clean internal interface;
 
 * prlim command for dealing with lots of subgoals (an easier way of
 setting goals_limit);
 
-*** Syntax
+
+*** Syntax ***
 
 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
 be used in conjunction with the Isabelle symbol font; uses the
@@ -28,7 +30,8 @@
 the current print_mode);
 
 * token translations for modes "xterm" and "xterm_color" that display
-names in bold, underline etc. or colors;
+names in bold, underline etc. or colors (which requires a color
+version of xterm);
 
 * now supports alternative (named) syntax tables (parser and pretty
 printer); internal interface is provided by add_modesyntax(_i);
@@ -38,6 +41,7 @@
 * added typed_print_translation (like print_translation, but may
 access type of constant);
 
+
 *** Classical Reasoner ***
 
 Blast_tac: a new tactic!  It is often more powerful than fast_tac, but has
@@ -63,8 +67,15 @@
 COULD MAKE EXISTING PROOFS FAIL; in case of problems with
 old proofs, use unsafe_addss and unsafe_auto_tac
 
+
 *** Simplifier ***
 
+* added interface for simplification procedures (functions that
+produce *proven* rewrite rules on the fly, depending on current
+redex);
+
+* ordering on terms as parameter (used for ordered rewriting);
+
 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
 
 * the solver is now split into a safe and an unsafe part.
@@ -72,9 +83,6 @@
 functions setsolver and addsolver have been renamed to setSolver and
 addSolver.  added safe_asm_full_simp_tac.
 
-* ordering on terms as parameter (used for ordered rewriting);
-added interface for simplification procedures (functions that produce *proven*
-rewrite rules on the fly, depending on current redex);
 
 *** HOL ***
 
@@ -105,6 +113,7 @@
   + eliminated blift from Lift3.thy (use Def instead of blift)
   all eliminated rules are derived as theorems --> no visible changes 
 
+
 *** ZF ***
 
 * ZF now has Fast_tac, Simp_tac and Auto_tac.  Union_iff is a now a default