equal
deleted
inserted
replaced
68 |
68 |
69 The header includes at least \<^verbatim>\<open>Title\<close> and \<^verbatim>\<open>Author\<close> entries, followed by a |
69 The header includes at least \<^verbatim>\<open>Title\<close> and \<^verbatim>\<open>Author\<close> entries, followed by a |
70 prose description of the purpose of the module. The latter can range from a |
70 prose description of the purpose of the module. The latter can range from a |
71 single line to several paragraphs of explanations. |
71 single line to several paragraphs of explanations. |
72 |
72 |
73 The rest of the file is divided into sections, subsections, subsubsections, |
73 The rest of the file is divided into chapters, sections, subsections, |
74 paragraphs etc.\ using a simple layout via ML comments as follows. |
74 subsubsections, paragraphs etc.\ using a simple layout via ML comments as |
|
75 follows. |
75 |
76 |
76 @{verbatim [display] |
77 @{verbatim [display] |
77 \<open> (*** section ***) |
78 \<open> (**** chapter ****) |
|
79 |
|
80 (*** section ***) |
78 |
81 |
79 (** subsection **) |
82 (** subsection **) |
80 |
83 |
81 (* subsubsection *) |
84 (* subsubsection *) |
82 |
85 |