equal
deleted
inserted
replaced
2 Isabelle NEWS -- history of user-visible changes |
2 Isabelle NEWS -- history of user-visible changes |
3 ================================================ |
3 ================================================ |
4 |
4 |
5 New in Isabelle???? (DATE ????) |
5 New in Isabelle???? (DATE ????) |
6 ------------------------------- |
6 ------------------------------- |
|
7 |
|
8 * replaced print_goals_ref hook by print_current_goals_fn and |
|
9 result_error_fn; |
7 |
10 |
8 * HOL/simplifier: terms of the form |
11 * HOL/simplifier: terms of the form |
9 `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x) |
12 `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x) |
10 are rewritten to |
13 are rewritten to |
11 `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)' |
14 `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)' |
12 |
15 |
13 * HOL/Lists: the function "set_of_list" has been renamed "set" (and its |
16 * HOL/Lists: the function "set_of_list" has been renamed "set" (and its |
14 theorems too) |
17 theorems too); |
15 |
18 |
16 * removed old README and Makefiles; |
19 * removed old README and Makefiles; |
17 |
20 |
18 * removed obsolete init_pps and init_database; |
21 * removed obsolete init_pps and init_database; |
19 |
22 |