equal
deleted
inserted
replaced
3 |
3 |
4 New in this Isabelle release |
4 New in this Isabelle release |
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** General *** |
7 *** General *** |
|
8 |
|
9 * Theory syntax: the header format ``theory A = B + C:'' has been |
|
10 discontinued in favour of ``theory A imports B C begin''. Use isatool |
|
11 fixheaders to convert existing theory files. INCOMPATIBILITY. |
|
12 |
|
13 * Theory syntax: the old non-Isar theory file format has been |
|
14 discontinued altogether. Note that ML proof scripts may still be used |
|
15 with Isar theories; migration is usually quite simple with the ML |
|
16 function use_legacy_bindings. INCOMPATIBILITY. |
|
17 |
|
18 * Legacy goal package: removed former user-level functions top_sg, |
|
19 prin, printyp, pprint_term/typ, which tend to cause confusion about |
|
20 the actual goal (!) context being used here. |
8 |
21 |
9 * Command 'find_theorems': support "*" wildcard in "name:" criterion. |
22 * Command 'find_theorems': support "*" wildcard in "name:" criterion. |
10 |
23 |
11 |
24 |
12 *** Document preparation *** |
25 *** Document preparation *** |