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