2 Isabelle NEWS -- history of user-visible changes |
2 Isabelle NEWS -- history of user-visible changes |
3 ================================================ |
3 ================================================ |
4 |
4 |
5 New in Isabelle94-8 (??????????? 1997 FIXME) |
5 New in Isabelle94-8 (??????????? 1997 FIXME) |
6 --------------------------------------- |
6 --------------------------------------- |
|
7 * HOLCF changes: derived all rules and arities |
|
8 + axiomatic type classes instead of classes |
|
9 + typedef instead of faking type definitions |
|
10 + eliminated the initernal constants less_fun, less_cfun, UU_fun, UU_cfun etc. |
|
11 + new axclasses cpo,chfin,flat with flat<chfin<pcpo<cpo<po |
|
12 + eliminated the types void, one, tr |
|
13 + use unit lift and bool lift (with translations) instead of one and tr |
|
14 + eliminated blift from Lift3.thy (use Def instead of blift) |
|
15 all eliminated rules are derivd as theorems --> no visible changes |
7 |
16 |
8 * simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss. |
17 * simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss. |
9 |
18 |
10 * simplifier: the solver is now split into a safe and an unsafe part. |
19 * simplifier: the solver is now split into a safe and an unsafe part. |
11 This should be invisible for the normal user, except that the functions |
20 This should be invisible for the normal user, except that the functions |
59 |
68 |
60 * more default rewrite rules in HOL for quantifiers, union/intersection; |
69 * more default rewrite rules in HOL for quantifiers, union/intersection; |
61 |
70 |
62 * the NEWS file; |
71 * the NEWS file; |
63 |
72 |
|
73 Changes in HOLCF: |
|
74 |
64 |
75 |
65 New in Isabelle94-7 (November 96) |
76 New in Isabelle94-7 (November 96) |
66 --------------------------------- |
77 --------------------------------- |
67 |
78 |
68 * allowing negative levels (as offsets) in prlev and choplev; |
79 * allowing negative levels (as offsets) in prlev and choplev; |