NEWS
changeset 2554 1b160cd50130
parent 2553 ed941505cab7
child 2555 29b27a74c7d8
     1.1 --- a/NEWS	Fri Jan 24 17:37:59 1997 +0100
     1.2 +++ b/NEWS	Fri Jan 24 18:24:04 1997 +0100
     1.3 @@ -2,8 +2,9 @@
     1.4  Isabelle NEWS -- history of user-visible changes
     1.5  ================================================
     1.6  
     1.7 -New in Isabelle94-8 (???????????)
     1.8 ----------------------------------
     1.9 +
    1.10 +New in Isabelle94-8 (??????????? 1997 FIXME)
    1.11 +---------------------------------------
    1.12  
    1.13  * the NEWS file;
    1.14  
    1.15 @@ -42,11 +43,67 @@
    1.16  * more default rewrite rules in HOL for quantifiers, union/intersection;
    1.17  
    1.18  
    1.19 +
    1.20  New in Isabelle94-7 (November 96)
    1.21  ---------------------------------
    1.22  
    1.23  * allowing negative levels (as offsets) in prlev and choplev;
    1.24  
    1.25 -* many more things we do not remember :-)
    1.26 +* super-linear speedup for large simplifications;
    1.27 +
    1.28 +* FOL, ZF and HOL now use miniscoping: rewriting pushes
    1.29 +quantifications in as far as possible (COULD MAKE EXISTING PROOFS
    1.30 +FAIL); can suppress it using the command Delsimps (ex_simps @
    1.31 +all_simps); De Morgan laws are also now included, by default;
    1.32 +
    1.33 +* improved printing of ==>  :  ~:
    1.34 +
    1.35 +* new object-logic "Sequents" adds linear logic, while replacing LK
    1.36 +and Modal (thanks to Sara Kalvala);
    1.37 +
    1.38 +* HOL/Auth: correctness proofs for authentication protocols;
    1.39 +
    1.40 +* HOL: new auto_tac combines rewriting and classical reasoning (many
    1.41 +examples on HOL/Auth);
    1.42 +
    1.43 +* HOL: new command AddIffs for declaring theorems of the form P=Q to
    1.44 +the rewriter and classical reasoner simultaneously;
    1.45 +
    1.46 +* function uresult no longer returns theorems in "standard" format;
    1.47 +regain previous version by: val uresult = standard o uresult;
    1.48 +
    1.49 +
    1.50 +
    1.51 +New in Isabelle94-6
    1.52 +-------------------
    1.53 +
    1.54 +* oracles -- these establish an interface between Isabelle and trusted
    1.55 +external reasoners, which may deliver results as theorems;
    1.56 +
    1.57 +* proof objects (in particular record all uses of oracles);
    1.58 +
    1.59 +* Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
    1.60 +
    1.61 +* "constdefs" section in theory files;
    1.62 +
    1.63 +* "primrec" section (HOL) no longer requires names;
    1.64 +
    1.65 +* internal type "tactic" now simply "thm -> thm Sequence.seq";
    1.66 +
    1.67 +
    1.68 +
    1.69 +New in Isabelle94-5
    1.70 +-------------------
    1.71 +
    1.72 +* reduced space requirements;
    1.73 +
    1.74 +* automatic HTML generation from theories;
    1.75 +
    1.76 +* theory files no longer require "..." (quotes) around most types;
    1.77 +
    1.78 +* new examples, including two proofs of the Church-Rosser theorem;
    1.79 +
    1.80 +* non-curried (1994) version of HOL is no longer distributed;
    1.81 +
    1.82  
    1.83  $Id$