src/Doc/System/Presentation.thy

   Produce the document from session \<^verbatim>\<open>FOL\<close> with full verbosity, and a copy in
   the current directory (subdirectory \<^verbatim>\<open>document\<close> and file \<^verbatim>\<open>document.pdf)\<close>:
 
   @{verbatim [display] \<open>isabelle document -v -V -O. FOL\<close>}
 \<close>
+
 
 section \<open>Full-text search for formal theory content\<close>
 
 text \<open>
   The session information of a regular @{tool_ref build} can also be used to