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