Isabelle NEWS -- history of user-visible changes================================================New in Isabelle94-8 (really-soon-now 1997 FIXME)------------------------------------------------* HOLCF changes: derived all rules and arities + axiomatic type classes instead of classes + typedef instead of faking type definitions + eliminated the initernal constants less_fun, less_cfun, UU_fun, UU_cfun etc. + new axclasses cpo,chfin,flat with flat<chfin<pcpo<cpo<po + eliminated the types void, one, tr + use unit lift and bool lift (with translations) instead of one and tr + eliminated blift from Lift3.thy (use Def instead of blift) all eliminated rules are derivd as theorems --> no visible changes * simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.* simplifier: the solver is now split into a safe and an unsafe part. This should be invisible for the normal user, except that the functions setsolver and addsolver have been renamed to setSolver and addSolver. added safe_asm_full_simp_tac. * classical reasoner: little changes in semantics of addafter (now: addaltern), renamed setwrapper to setWrapper, addwrapper to addWrapper added safe wrapper (and access functions for it)* improved combination of classical reasoner and simplifier: new addss, auto_tac, functions for handling clasimpsets, ... Now, the simplification is safe (therefore moved to safe_step_tac) and thus more complete, as multiple instantiation of unknowns (with slow_tac) possible COULD MAKE EXISTING PROOFS FAIL; in case of problems with unstable old proofs: use unsafe_addss and unsafe_auto_tac* HOL: primrec now also works with type nat;* new utilities to build / run / maintain Isabelle etc. (in partsstill somewhat experimental); old Makefiles etc. still functional;* simplifier: termless order as parameter; added interface forsimplification procedures (functions that produce *proven* rewriterules on the fly, depending on current redex);* now supports alternative (named) syntax tables (parser and prettyprinter); internal interface is provided by add_modesyntax(_i);* Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; tobe used in conjunction with the isabelle symbol font; uses the"symbols" syntax table;* infixes may now be declared with names independent of their syntax;* added typed_print_translation (like print_translation, but mayaccess type of constant);* prlim command for dealing with lots of subgoals (an easier way ofsetting goals_limit);* HOL/ex/Ring.thy declares cring_simp, which solves equationalproblems in commutative rings, using axiomatic type classes for + and *;* ZF now has Fast_tac, Simp_tac and Auto_tac. WARNING: don't useZF.thy anymore! Contains fewer defs and could make a bogus simpset.Beware of Union_iff. eq_cs is gone, can be put back as ZF_cs addSIs[equalityI];* more examples in HOL/MiniML and HOL/Auth;* more default rewrite rules in HOL for quantifiers, union/intersection;* the NEWS file;New in Isabelle94-7 (November 96)---------------------------------* allowing negative levels (as offsets) in prlev and choplev;* super-linear speedup for large simplifications;* FOL, ZF and HOL now use miniscoping: rewriting pushesquantifications in as far as possible (COULD MAKE EXISTING PROOFSFAIL); can suppress it using the command Delsimps (ex_simps @all_simps); De Morgan laws are also now included, by default;* improved printing of ==> : ~:* new object-logic "Sequents" adds linear logic, while replacing LKand Modal (thanks to Sara Kalvala);* HOL/Auth: correctness proofs for authentication protocols;* HOL: new auto_tac combines rewriting and classical reasoning (manyexamples on HOL/Auth);* HOL: new command AddIffs for declaring theorems of the form P=Q tothe rewriter and classical reasoner simultaneously;* function uresult no longer returns theorems in "standard" format;regain previous version by: val uresult = standard o uresult;New in Isabelle94-6-------------------* oracles -- these establish an interface between Isabelle and trustedexternal reasoners, which may deliver results as theorems;* proof objects (in particular record all uses of oracles);* Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;* "constdefs" section in theory files;* "primrec" section (HOL) no longer requires names;* internal type "tactic" now simply "thm -> thm Sequence.seq";New in Isabelle94-5-------------------* reduced space requirements;* automatic HTML generation from theories;* theory files no longer require "..." (quotes) around most types;* new examples, including two proofs of the Church-Rosser theorem;* 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 theAxiom 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 andtranslates 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 repeatedfreely;* Database of theorems for FOL, HOL and ZF. Newcommands including qed, qed_goal and bind_thm store theorems in the database.* Simple database queries: return a named theorem (get_thm) or all theorems ofa 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_csand HOL_dup_cs obsolete;* Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1have 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 existingtypes;$Id$