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$