equal
deleted
inserted
replaced
555 syntax constant (cf. 'syntax' command). |
555 syntax constant (cf. 'syntax' command). |
556 |
556 |
557 * Antiquotation @{make_string} inlines a function to print arbitrary |
557 * Antiquotation @{make_string} inlines a function to print arbitrary |
558 values similar to the ML toplevel. The result is compiler dependent |
558 values similar to the ML toplevel. The result is compiler dependent |
559 and may fall back on "?" in certain situations. |
559 and may fall back on "?" in certain situations. |
|
560 |
|
561 * Diagnostic commands 'ML_val' and 'ML_command' may refer to |
|
562 antiquotations @{Isar.state} and @{Isar.goal}. This replaces impure |
|
563 Isar.state() and Isar.goal(), which belong to the old TTY loop and do |
|
564 not work with the asynchronous Isar document model. |
560 |
565 |
561 * Sorts.certify_sort and derived "cert" operations for types and terms |
566 * Sorts.certify_sort and derived "cert" operations for types and terms |
562 no longer minimize sorts. Thus certification at the boundary of the |
567 no longer minimize sorts. Thus certification at the boundary of the |
563 inference kernel becomes invariant under addition of class relations, |
568 inference kernel becomes invariant under addition of class relations, |
564 which is an important monotonicity principle. Sorts are now minimized |
569 which is an important monotonicity principle. Sorts are now minimized |