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 * Document antiquotations for ML text have been refined: "def" and "ref" |
|
38 variants support index entries, e.g. @{ML} (no entry) vs. @{ML_def} |
|
39 (bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit |
|
40 type arguments for constructors (only relevant for index), e.g. |
|
41 @{ML_type \<open>'a list\<close>} vs. @{ML_type 'a \<open>list\<close>}; @{ML_op} has been renamed |
|
42 to @{ML_infix}. Minor INCOMPATIBILITY concerning name and syntax. |
36 |
43 |
37 * Option "document_logo" determines if an instance of the Isabelle logo |
44 * Option "document_logo" determines if an instance of the Isabelle logo |
38 should be created in the document output directory. The given string |
45 should be created in the document output directory. The given string |
39 specifies the name of the logo variant, while "_" (underscore) refers to |
46 specifies the name of the logo variant, while "_" (underscore) refers to |
40 the unnamed variant. The output file name is always "isabelle_logo.pdf". |
47 the unnamed variant. The output file name is always "isabelle_logo.pdf". |