equal
deleted
inserted
replaced
518 |
518 |
519 * All constant names are now qualified. INCOMPATIBILITY. |
519 * All constant names are now qualified. INCOMPATIBILITY. |
520 |
520 |
521 |
521 |
522 *** ML *** |
522 *** ML *** |
|
523 |
|
524 * Former exception Library.UnequalLengths now coincides with |
|
525 ListPair.UnequalLengths. |
523 |
526 |
524 * Renamed raw "explode" function to "raw_explode" to emphasize its |
527 * Renamed raw "explode" function to "raw_explode" to emphasize its |
525 meaning. Note that internally to Isabelle, Symbol.explode is used in |
528 meaning. Note that internally to Isabelle, Symbol.explode is used in |
526 almost all situations. |
529 almost all situations. |
527 |
530 |