equal
deleted
inserted
replaced
10 INCOMPATIBILITY in identifier syntax etc. |
10 INCOMPATIBILITY in identifier syntax etc. |
11 |
11 |
12 * Outer syntax: string tokens may contain arbitrary character codes |
12 * Outer syntax: string tokens may contain arbitrary character codes |
13 specified via 3 decimal digits (as in SML). E.g. "foo\095bar" for |
13 specified via 3 decimal digits (as in SML). E.g. "foo\095bar" for |
14 "foo_bar". |
14 "foo_bar". |
|
15 |
|
16 * Outer syntax: string tokens no longer admit escaped white space, |
|
17 which was an accidental (undocumented) feature. INCOMPATIBILITY, use |
|
18 white space directly. |
15 |
19 |
16 * Theory loader: use_thy (and similar operations) no longer set the |
20 * Theory loader: use_thy (and similar operations) no longer set the |
17 implicit ML context, which was occasionally hard to predict and in |
21 implicit ML context, which was occasionally hard to predict and in |
18 conflict with concurrency. INCOMPATIBILITY, use ML within Isar which |
22 conflict with concurrency. INCOMPATIBILITY, use ML within Isar which |
19 provides a proper context already. |
23 provides a proper context already. |