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 Isabelle???? (DATE ????) |
5 New in Isabelle98 (January 1998) |
6 ------------------------------- |
6 -------------------------------- |
|
7 |
|
8 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
|
9 |
|
10 * changed lexical syntax of terms / types: dots made part of long |
|
11 identifiers, e.g. "%x.x" no longer possible, should be "%x. x"; |
|
12 |
|
13 * simpset (and claset) reference variable replaced by functions |
|
14 simpset / simpset_ref; |
|
15 |
|
16 * no longer supports theory aliases (via merge) and non-trivial |
|
17 implicit merge of thms' signatures; |
|
18 |
|
19 * most internal names of constants changed due to qualified names; |
|
20 |
|
21 * changed Pure/Sequence interface (see Pure/seq.ML); |
|
22 |
7 |
23 |
8 *** General Changes *** |
24 *** General Changes *** |
9 |
25 |
10 * hierachically structured name spaces (for consts, types, axms, thms |
26 * hierachically structured name spaces (for consts, types, axms, thms |
11 etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of |
27 etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of |