|
2553
|
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$
|