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 