# 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 ; + +* 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$