# HG changeset patch
# User paulson
# Date 857726364 -3600
# Node ID 9fdc1461085fa38a02ad2406d09c64b567d8a2f0
# Parent  2a2d51f2cd955b537361e5b28e04d9995a60bd6a
Tidied and updated

diff -r 2a2d51f2cd95 -r 9fdc1461085f NEWS
--- a/NEWS	Fri Mar 07 09:56:55 1997 +0100
+++ b/NEWS	Fri Mar 07 10:19:24 1997 +0100
@@ -14,12 +14,12 @@
 * HOLCF changes: derived all rules and arities 
   + axiomatic type classes instead of classes 
   + typedef instead of faking type definitions
-  + eliminated the initernal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
+  + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
   + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
   + eliminated the types void, one, tr
   + use unit lift and bool lift (with translations) instead of one and tr
   + eliminated blift from Lift3.thy (use Def instead of blift)
-  all eliminated rules are derivd as theorems --> no visible changes 
+  all eliminated rules are derived as theorems --> no visible changes 
 
 * simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
 
@@ -28,16 +28,19 @@
 functions setsolver and addsolver have been renamed to setSolver and
 addSolver.  added safe_asm_full_simp_tac.
 
-* classical reasoner: little changes in semantics of addafter (now:
-addaltern), renamed setwrapper to setWrapper, addwrapper to addWrapper
+* classical reasoner: substitution with equality assumptions no longer
+permutes other assumptions.
+
+* classical reasoner: minor changes in semantics of addafter (now called
+addaltern); renamed setwrapper to setWrapper and addwrapper to addWrapper;
 added safe wrapper (and access functions for it)
 
 * improved combination of classical reasoner and simplifier: new
 addss, auto_tac, functions for handling clasimpsets, ...  Now, the
 simplification is safe (therefore moved to safe_step_tac) and thus
-more complete, as multiple instantiation of unknowns (with slow_tac)
-possible COULD MAKE EXISTING PROOFS FAIL; in case of problems with
-unstable old proofs: use unsafe_addss and unsafe_auto_tac
+more complete, as multiple instantiation of unknowns (with slow_tac).
+COULD MAKE EXISTING PROOFS FAIL; in case of problems with
+old proofs, use unsafe_addss and unsafe_auto_tac
 
 * HOL: primrec now also works with type nat;
 
@@ -55,7 +58,7 @@
 printer); internal interface is provided by add_modesyntax(_i);
 
 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
-be used in conjunction with the isabelle symbol font; uses the
+be used in conjunction with the Isabelle symbol font; uses the
 "symbols" syntax table;
 
 * infixes may now be declared with names independent of their syntax;
@@ -148,7 +151,7 @@
 New in Isabelle94-4
 -------------------
 
-* greatly space requirements;
+* greatly reduced space requirements;
 
 * theory files (.thy) no longer require \...\ escapes at line breaks;