# HG changeset patch
# User paulson
# Date 854373677 -3600
# Node ID dffebc6ab0a1cf97fc71c0729b83422306009748
# Parent  bef8e1315cbc0b3dfe1d0af92b8474be4fe2c6df
More news items, dating back to 1995

diff -r bef8e1315cbc -r dffebc6ab0a1 NEWS
--- a/NEWS	Mon Jan 27 09:08:54 1997 +0100
+++ b/NEWS	Mon Jan 27 15:01:17 1997 +0100
@@ -107,4 +107,85 @@
 * non-curried (1994) version of HOL is no longer distributed;
 
 
+
+New in Isabelle94-4
+-------------------
+
+* greatly space requirements;
+
+* theory files (.thy) no longer require \...\ escapes at line breaks;
+
+* searchable theorem database (see the section "Retrieving theorems" on 
+page 8 of the Reference Manual);
+
+* new examples, including Grabczewski's monumental case study of the
+Axiom of Choice;
+
+* The previous version of HOL renamed to Old_HOL;
+
+* The new version of HOL (previously called CHOL) uses a curried syntax 
+for functions.  Application looks like f a b instead of f(a,b);
+
+* Mutually recursive inductive definitions finally work in HOL;
+
+* In ZF, pattern-matching on tuples is now available in all abstractions and
+translates to the operator "split";
+
+
+
+New in Isabelle94-3
+-------------------
+
+* new infix operator, addss, allowing the classical reasoner to 
+perform simplification at each step of its search.  Example:
+	fast_tac (cs addss ss)
+
+* a new logic, CHOL, the same as HOL, but with a curried syntax 
+for functions.  Application looks like f a b instead of f(a,b).  Also pairs 
+look like (a,b) instead of <a,b>;
+
+* PLEASE NOTE: CHOL will eventually replace HOL!
+
+* In CHOL, pattern-matching on tuples is now available in all abstractions.
+It translates to the operator "split".  A new theory of integers is available;
+
+* In ZF, integer numerals now denote two's-complement binary integers.
+Arithmetic operations can be performed by rewriting.  See ZF/ex/Bin.ML;
+
+* Many new examples: I/O automata, Church-Rosser theorem, equivalents 
+of the Axiom of Choice;
+
+
+
+New in Isabelle94-2
+-------------------
+
+* Significantly faster resolution;  
+
+* the different sections in a .thy file can now be mixed and repeated
+freely;
+
+* Database of theorems for FOL, HOL and ZF.  New
+commands including qed, qed_goal and bind_thm store theorems in the database.
+
+* Simple database queries: return a named theorem (get_thm) or all theorems of
+a given theory (thms_of), or find out what theory a theorem was proved in
+(theory_of_thm);
+
+* Bugs fixed in the inductive definition and datatype packages;
+
+* The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
+and HOL_dup_cs obsolete;
+
+* Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
+have been removed;
+
+* Simpler definition of function space in ZF;
+
+* new results about cardinal and ordinal arithmetic in ZF;
+
+* 'subtype' facility in HOL for introducing new types as subsets of existing
+types;
+
+
 $Id$