NEWS
author wenzelm
Fri Jan 24 17:37:59 1997 +0100 (1997-01-24)
changeset 2553 ed941505cab7
child 2554 1b160cd50130
permissions -rw-r--r--
Isabelle NEWS -- history of user-visible changes;
     1 
     2 Isabelle NEWS -- history of user-visible changes
     3 ================================================
     4 
     5 New in Isabelle94-8 (???????????)
     6 ---------------------------------
     7 
     8 * the NEWS file;
     9 
    10 * new utilities to build / run / maintain Isabelle etc. (in parts
    11 still somewhat experimental);
    12 
    13 * simplifier: termless order as parameter; added interface for
    14 simplification procedures (functions that produce *proven* rewrite
    15 rules on the fly, depending on current redex);
    16 
    17 * now supports alternative (named) syntax tables (parser and pretty
    18 printer); internal interface is provided by add_modesyntax(_i);
    19 
    20 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
    21 be used in conjunction with the isabelle symbol font; uses the
    22 "symbols" syntax table;
    23 
    24 * infixes may now be declared with names independent of their syntax;
    25 
    26 * added typed_print_translation (like print_translation, but also gets
    27 the type of the constant);
    28 
    29 * prlim command for dealing with lots of subgoals (an easier way of
    30 setting goals_limit);
    31 
    32 * HOL/ex/Ring.thy declares cring_simp, which solves equational
    33 problems in commutative rings, using axiomatic type classes for + and *;
    34 
    35 * ZF now has Fast_tac, Simp_tac and Auto_tac.  WARNING: don't use
    36 ZF.thy anymore!  Contains fewer defs and could make a bogus simpset.
    37 Beware of Union_iff.  eq_cs is gone, can be put back as ZF_cs addSIs
    38 [equalityI];
    39 
    40 * more examples in HOL/MiniML and HOL/Auth;
    41 
    42 * more default rewrite rules in HOL for quantifiers, union/intersection;
    43 
    44 
    45 New in Isabelle94-7 (November 96)
    46 ---------------------------------
    47 
    48 * allowing negative levels (as offsets) in prlev and choplev;
    49 
    50 * many more things we do not remember :-)
    51 
    52 $Id$