equal
deleted
inserted
replaced
487 |
487 |
488 * All constant names are now qualified. INCOMPATIBILITY. |
488 * All constant names are now qualified. INCOMPATIBILITY. |
489 |
489 |
490 |
490 |
491 *** ML *** |
491 *** ML *** |
|
492 |
|
493 * Renamed raw "explode" function to "raw_explode" to emphasize its |
|
494 meaning. Note that internally to Isabelle, Symbol.explode is used in |
|
495 almost all situations. |
492 |
496 |
493 * Discontinued obsolete function sys_error and exception SYS_ERROR. |
497 * Discontinued obsolete function sys_error and exception SYS_ERROR. |
494 See implementation manual for further details on exceptions in |
498 See implementation manual for further details on exceptions in |
495 Isabelle/ML. |
499 Isabelle/ML. |
496 |
500 |