equal
deleted
inserted
replaced
11 non-ASCII bytes as before. Since Isabelle/ML string literals may |
11 non-ASCII bytes as before. Since Isabelle/ML string literals may |
12 contain symbols without further backslash escapes, Unicode can now be |
12 contain symbols without further backslash escapes, Unicode can now be |
13 used here as well. Recall that Symbol.explode in ML provides a |
13 used here as well. Recall that Symbol.explode in ML provides a |
14 consistent view on symbols, while raw explode (or String.explode) |
14 consistent view on symbols, while raw explode (or String.explode) |
15 merely give a byte-oriented representation. |
15 merely give a byte-oriented representation. |
|
16 |
|
17 * Theory loading: only the master source file is looked-up in the |
|
18 implicit load path, all other files are addressed relatively to its |
|
19 directory. Minor INCOMPATIBILITY, subtle change in semantics. |
16 |
20 |
17 * Special treatment of ML file names has been discontinued. |
21 * Special treatment of ML file names has been discontinued. |
18 Historically, optional extensions .ML or .sml were added on demand -- |
22 Historically, optional extensions .ML or .sml were added on demand -- |
19 at the cost of clarity of file dependencies. Recall that Isabelle/ML |
23 at the cost of clarity of file dependencies. Recall that Isabelle/ML |
20 files exclusively use the .ML extension. Minor INCOMPATIBILTY. |
24 files exclusively use the .ML extension. Minor INCOMPATIBILTY. |