NEWS
 changeset 2557 dffebc6ab0a1 parent 2556 bef8e1315cbc child 2639 2c38796b33b9
```     1.1 --- a/NEWS	Mon Jan 27 09:08:54 1997 +0100
1.2 +++ b/NEWS	Mon Jan 27 15:01:17 1997 +0100
1.3 @@ -107,4 +107,85 @@
1.4  * non-curried (1994) version of HOL is no longer distributed;
1.5
1.6
1.7 +
1.8 +New in Isabelle94-4
1.9 +-------------------
1.10 +
1.11 +* greatly space requirements;
1.12 +
1.13 +* theory files (.thy) no longer require \...\ escapes at line breaks;
1.14 +
1.15 +* searchable theorem database (see the section "Retrieving theorems" on
1.16 +page 8 of the Reference Manual);
1.17 +
1.18 +* new examples, including Grabczewski's monumental case study of the
1.19 +Axiom of Choice;
1.20 +
1.21 +* The previous version of HOL renamed to Old_HOL;
1.22 +
1.23 +* The new version of HOL (previously called CHOL) uses a curried syntax
1.24 +for functions.  Application looks like f a b instead of f(a,b);
1.25 +
1.26 +* Mutually recursive inductive definitions finally work in HOL;
1.27 +
1.28 +* In ZF, pattern-matching on tuples is now available in all abstractions and
1.29 +translates to the operator "split";
1.30 +
1.31 +
1.32 +
1.33 +New in Isabelle94-3
1.34 +-------------------
1.35 +
1.36 +* new infix operator, addss, allowing the classical reasoner to
1.37 +perform simplification at each step of its search.  Example:
1.38 +	fast_tac (cs addss ss)
1.39 +
1.40 +* a new logic, CHOL, the same as HOL, but with a curried syntax
1.41 +for functions.  Application looks like f a b instead of f(a,b).  Also pairs
1.42 +look like (a,b) instead of <a,b>;
1.43 +
1.44 +* PLEASE NOTE: CHOL will eventually replace HOL!
1.45 +
1.46 +* In CHOL, pattern-matching on tuples is now available in all abstractions.
1.47 +It translates to the operator "split".  A new theory of integers is available;
1.48 +
1.49 +* In ZF, integer numerals now denote two's-complement binary integers.
1.50 +Arithmetic operations can be performed by rewriting.  See ZF/ex/Bin.ML;
1.51 +
1.52 +* Many new examples: I/O automata, Church-Rosser theorem, equivalents
1.53 +of the Axiom of Choice;
1.54 +
1.55 +
1.56 +
1.57 +New in Isabelle94-2
1.58 +-------------------
1.59 +
1.60 +* Significantly faster resolution;
1.61 +
1.62 +* the different sections in a .thy file can now be mixed and repeated
1.63 +freely;
1.64 +
1.65 +* Database of theorems for FOL, HOL and ZF.  New
1.66 +commands including qed, qed_goal and bind_thm store theorems in the database.
1.67 +
1.68 +* Simple database queries: return a named theorem (get_thm) or all theorems of
1.69 +a given theory (thms_of), or find out what theory a theorem was proved in
1.70 +(theory_of_thm);
1.71 +
1.72 +* Bugs fixed in the inductive definition and datatype packages;
1.73 +
1.74 +* The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
1.75 +and HOL_dup_cs obsolete;
1.76 +
1.77 +* Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
1.78 +have been removed;
1.79 +
1.80 +* Simpler definition of function space in ZF;
1.81 +
1.82 +* new results about cardinal and ordinal arithmetic in ZF;
1.83 +
1.84 +* 'subtype' facility in HOL for introducing new types as subsets of existing
1.85 +types;
1.86 +
1.87 +
1.88  \$Id\$
```