NEWS
changeset 73830 2a431e8bb9b4
parent 73829 aefa7d210725
child 73842 9134ae401ad5
equal deleted inserted replaced
73829:aefa7d210725 73830:2a431e8bb9b4
    32 * More robust 'proof' outline for method "induct": support nested cases.
    32 * More robust 'proof' outline for method "induct": support nested cases.
    33 
    33 
    34 
    34 
    35 *** Document preparation ***
    35 *** Document preparation ***
    36 
    36 
    37 * More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (package
    37 * More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (LaTeX package
    38 "pifont").
    38 "pifont").
    39 
    39 
    40 * High-quality blackboard-bold symbols from font "txmia" (package
    40 * High-quality blackboard-bold symbols from font "txmia" (LaTeX package
    41 "pxfonts"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>.
    41 "pxfonts"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>.
    42 
    42 
    43 * Document antiquotations for ML text have been refined: "def" and "ref"
    43 * Document antiquotations for ML text have been refined: "def" and "ref"
    44 variants support index entries, e.g. @{ML} (no entry) vs. @{ML_def}
    44 variants support index entries, e.g. @{ML} (no entry) vs. @{ML_def}
    45 (bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit
    45 (bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit