equal
deleted
inserted
replaced
7 --------------------------------------- |
7 --------------------------------------- |
8 |
8 |
9 * the NEWS file; |
9 * the NEWS file; |
10 |
10 |
11 * new utilities to build / run / maintain Isabelle etc. (in parts |
11 * new utilities to build / run / maintain Isabelle etc. (in parts |
12 still somewhat experimental); |
12 still somewhat experimental); old Makefiles etc. still functional; |
13 |
13 |
14 * simplifier: termless order as parameter; added interface for |
14 * simplifier: termless order as parameter; added interface for |
15 simplification procedures (functions that produce *proven* rewrite |
15 simplification procedures (functions that produce *proven* rewrite |
16 rules on the fly, depending on current redex); |
16 rules on the fly, depending on current redex); |
17 |
17 |
22 be used in conjunction with the isabelle symbol font; uses the |
22 be used in conjunction with the isabelle symbol font; uses the |
23 "symbols" syntax table; |
23 "symbols" syntax table; |
24 |
24 |
25 * infixes may now be declared with names independent of their syntax; |
25 * infixes may now be declared with names independent of their syntax; |
26 |
26 |
27 * added typed_print_translation (like print_translation, but also gets |
27 * added typed_print_translation (like print_translation, but may |
28 the type of the constant); |
28 access type of constant); |
29 |
29 |
30 * prlim command for dealing with lots of subgoals (an easier way of |
30 * prlim command for dealing with lots of subgoals (an easier way of |
31 setting goals_limit); |
31 setting goals_limit); |
32 |
32 |
33 * HOL/ex/Ring.thy declares cring_simp, which solves equational |
33 * HOL/ex/Ring.thy declares cring_simp, which solves equational |