--- a/src/Doc/Implementation/ML.thy Thu Aug 04 21:30:20 2016 +0200
+++ b/src/Doc/Implementation/ML.thy Fri Aug 05 16:30:53 2016 +0200
@@ -70,11 +70,14 @@
prose description of the purpose of the module. The latter can range from a
single line to several paragraphs of explanations.
- The rest of the file is divided into sections, subsections, subsubsections,
- paragraphs etc.\ using a simple layout via ML comments as follows.
+ The rest of the file is divided into chapters, sections, subsections,
+ subsubsections, paragraphs etc.\ using a simple layout via ML comments as
+ follows.
@{verbatim [display]
-\<open> (*** section ***)
+\<open> (**** chapter ****)
+
+ (*** section ***)
(** subsection **)