NEWS
changeset 2553 ed941505cab7
child 2554 1b160cd50130
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/NEWS	Fri Jan 24 17:37:59 1997 +0100
     1.3 @@ -0,0 +1,52 @@
     1.4 +
     1.5 +Isabelle NEWS -- history of user-visible changes
     1.6 +================================================
     1.7 +
     1.8 +New in Isabelle94-8 (???????????)
     1.9 +---------------------------------
    1.10 +
    1.11 +* the NEWS file;
    1.12 +
    1.13 +* new utilities to build / run / maintain Isabelle etc. (in parts
    1.14 +still somewhat experimental);
    1.15 +
    1.16 +* simplifier: termless order as parameter; added interface for
    1.17 +simplification procedures (functions that produce *proven* rewrite
    1.18 +rules on the fly, depending on current redex);
    1.19 +
    1.20 +* now supports alternative (named) syntax tables (parser and pretty
    1.21 +printer); internal interface is provided by add_modesyntax(_i);
    1.22 +
    1.23 +* Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
    1.24 +be used in conjunction with the isabelle symbol font; uses the
    1.25 +"symbols" syntax table;
    1.26 +
    1.27 +* infixes may now be declared with names independent of their syntax;
    1.28 +
    1.29 +* added typed_print_translation (like print_translation, but also gets
    1.30 +the type of the constant);
    1.31 +
    1.32 +* prlim command for dealing with lots of subgoals (an easier way of
    1.33 +setting goals_limit);
    1.34 +
    1.35 +* HOL/ex/Ring.thy declares cring_simp, which solves equational
    1.36 +problems in commutative rings, using axiomatic type classes for + and *;
    1.37 +
    1.38 +* ZF now has Fast_tac, Simp_tac and Auto_tac.  WARNING: don't use
    1.39 +ZF.thy anymore!  Contains fewer defs and could make a bogus simpset.
    1.40 +Beware of Union_iff.  eq_cs is gone, can be put back as ZF_cs addSIs
    1.41 +[equalityI];
    1.42 +
    1.43 +* more examples in HOL/MiniML and HOL/Auth;
    1.44 +
    1.45 +* more default rewrite rules in HOL for quantifiers, union/intersection;
    1.46 +
    1.47 +
    1.48 +New in Isabelle94-7 (November 96)
    1.49 +---------------------------------
    1.50 +
    1.51 +* allowing negative levels (as offsets) in prlev and choplev;
    1.52 +
    1.53 +* many more things we do not remember :-)
    1.54 +
    1.55 +$Id$