1 |
1 |
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 (really-soon-now 1997 FIXME) |
5 New in Isabelle94-8 (April 1997) |
6 ------------------------------------------------ |
6 ------------------------------------------------ |
7 |
7 |
8 * added token_translation interface (may translate name tokens in |
8 * added token_translation interface (may translate name tokens in |
9 arbitrary ways, dependent on their type (free, bound, tfree, ...)); |
9 arbitrary ways, dependent on their type (free, bound, tfree, ...)); |
|
10 |
|
11 * token translations for modes "xterm" and "xterm_color" that display |
|
12 names in bold, underline etc. or colors; |
10 |
13 |
11 * HOLCF changes: derived all rules and arities |
14 * HOLCF changes: derived all rules and arities |
12 + axiomatic type classes instead of classes |
15 + axiomatic type classes instead of classes |
13 + typedef instead of faking type definitions |
16 + typedef instead of faking type definitions |
14 + eliminated the initernal constants less_fun, less_cfun, UU_fun, UU_cfun etc. |
17 + eliminated the initernal constants less_fun, less_cfun, UU_fun, UU_cfun etc. |
15 + new axclasses cpo,chfin,flat with flat<chfin<pcpo<cpo<po |
18 + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po |
16 + eliminated the types void, one, tr |
19 + eliminated the types void, one, tr |
17 + use unit lift and bool lift (with translations) instead of one and tr |
20 + use unit lift and bool lift (with translations) instead of one and tr |
18 + eliminated blift from Lift3.thy (use Def instead of blift) |
21 + eliminated blift from Lift3.thy (use Def instead of blift) |
19 all eliminated rules are derivd as theorems --> no visible changes |
22 all eliminated rules are derivd as theorems --> no visible changes |
20 |
23 |
32 * improved combination of classical reasoner and simplifier: |
35 * improved combination of classical reasoner and simplifier: |
33 new addss, auto_tac, functions for handling clasimpsets, ... |
36 new addss, auto_tac, functions for handling clasimpsets, ... |
34 Now, the simplification is safe (therefore moved to safe_step_tac) and thus |
37 Now, the simplification is safe (therefore moved to safe_step_tac) and thus |
35 more complete, as multiple instantiation of unknowns (with slow_tac) possible |
38 more complete, as multiple instantiation of unknowns (with slow_tac) possible |
36 COULD MAKE EXISTING PROOFS FAIL; in case of problems with unstable old proofs: |
39 COULD MAKE EXISTING PROOFS FAIL; in case of problems with unstable old proofs: |
37 use unsafe_addss and unsafe_auto_tac |
40 use unsafe_addss and unsafe_auto_tac |
38 |
41 |
39 * HOL: primrec now also works with type nat; |
42 * HOL: primrec now also works with type nat; |
40 |
43 |
41 * HOL: the constant for negation has been renamed from "not" to "Not" to |
44 * HOL: the constant for negation has been renamed from "not" to "Not" to |
42 harmonize with FOL, ZF, LK, etc. |
45 harmonize with FOL, ZF, LK, etc. |