src/Doc/Isar_Ref/Document_Preparation.thy

   Some tags are pre-declared for certain classes of commands, serving as
   default markup if no tags are given in the text:
 
   \<^medskip>
   \begin{tabular}{ll}
+    \<open>document\<close> & document markup commands \\
     \<open>theory\<close> & theory begin/end \\
     \<open>proof\<close> & all proof commands \\
     \<open>ML\<close> & all commands involving ML code \\
   \end{tabular}
   \<^medskip>