equal
deleted
inserted
replaced
31 |
31 |
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 |
|
37 * More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (package |
|
38 "pifont"). |
|
39 |
|
40 * High-quality blackboard-bold symbols from font "txmia" (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>. |
36 |
42 |
37 * Document antiquotations for ML text have been refined: "def" and "ref" |
43 * Document antiquotations for ML text have been refined: "def" and "ref" |
38 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} |
39 (bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit |
45 (bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit |
40 type arguments for constructors (only relevant for index), e.g. |
46 type arguments for constructors (only relevant for index), e.g. |
994 this more conservative (as in Java 8). Depending on the GTK theme |
1000 this more conservative (as in Java 8). Depending on the GTK theme |
995 configuration, "-Djdk.gtk.version=3" might work better or worse. |
1001 configuration, "-Djdk.gtk.version=3" might work better or worse. |
996 |
1002 |
997 |
1003 |
998 *** Document preparation *** |
1004 *** Document preparation *** |
999 |
|
1000 * More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (package |
|
1001 "pifont"). |
|
1002 |
|
1003 * High-quality blackboard-bold symbols from font "txmia" (package |
|
1004 "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>. |
|
1005 |
1005 |
1006 * Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that |
1006 * Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that |
1007 are stripped from document output: the effect is to modify the semantic |
1007 are stripped from document output: the effect is to modify the semantic |
1008 presentation context or to emit markup to the PIDE document. Some |
1008 presentation context or to emit markup to the PIDE document. Some |
1009 predefined markers are taken from the Dublin Core Metadata Initiative, |
1009 predefined markers are taken from the Dublin Core Metadata Initiative, |