summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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$