# HG changeset patch
# User wenzelm
# Date 854126644 -3600
# Node ID 1b160cd5013072d86ab624864eef53067a84b89b
# Parent  ed941505cab79ddf7700a0840c07397010750a80
*** empty log message ***

diff -r ed941505cab7 -r 1b160cd50130 NEWS
--- a/NEWS	Fri Jan 24 17:37:59 1997 +0100
+++ b/NEWS	Fri Jan 24 18:24:04 1997 +0100
@@ -2,8 +2,9 @@
 Isabelle NEWS -- history of user-visible changes
 ================================================
 
-New in Isabelle94-8 (???????????)
----------------------------------
+
+New in Isabelle94-8 (??????????? 1997 FIXME)
+---------------------------------------
 
 * the NEWS file;
 
@@ -42,11 +43,67 @@
 * more default rewrite rules in HOL for quantifiers, union/intersection;
 
 
+
 New in Isabelle94-7 (November 96)
 ---------------------------------
 
 * allowing negative levels (as offsets) in prlev and choplev;
 
-* many more things we do not remember :-)
+* super-linear speedup for large simplifications;
+
+* FOL, ZF and HOL now use miniscoping: rewriting pushes
+quantifications in as far as possible (COULD MAKE EXISTING PROOFS
+FAIL); can suppress it using the command Delsimps (ex_simps @
+all_simps); De Morgan laws are also now included, by default;
+
+* improved printing of ==>  :  ~:
+
+* new object-logic "Sequents" adds linear logic, while replacing LK
+and Modal (thanks to Sara Kalvala);
+
+* HOL/Auth: correctness proofs for authentication protocols;
+
+* HOL: new auto_tac combines rewriting and classical reasoning (many
+examples on HOL/Auth);
+
+* HOL: new command AddIffs for declaring theorems of the form P=Q to
+the rewriter and classical reasoner simultaneously;
+
+* function uresult no longer returns theorems in "standard" format;
+regain previous version by: val uresult = standard o uresult;
+
+
+
+New in Isabelle94-6
+-------------------
+
+* oracles -- these establish an interface between Isabelle and trusted
+external reasoners, which may deliver results as theorems;
+
+* proof objects (in particular record all uses of oracles);
+
+* Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
+
+* "constdefs" section in theory files;
+
+* "primrec" section (HOL) no longer requires names;
+
+* internal type "tactic" now simply "thm -> thm Sequence.seq";
+
+
+
+New in Isabelle94-5
+-------------------
+
+* reduced space requirements;
+
+* automatic HTML generation from theories;
+
+* theory files no longer require "..." (quotes) around most types;
+
+* new examples, including two proofs of the Church-Rosser theorem;
+
+* non-curried (1994) version of HOL is no longer distributed;
+
 
 $Id$