diff -r 866f6d5baf4c -r a5e3ba7cbb2a doc-src/System/Thy/document/Presentation.tex
--- a/doc-src/System/Thy/document/Presentation.tex	Tue Aug 07 23:38:18 2012 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex	Tue Aug 07 23:43:05 2012 +0200
@@ -257,8 +257,7 @@
   manual editing of the generated \verb|IsaMakefile|, which is
   meant to cover all of the sub-session directories at the same time
   (this is the deeper reasong why \verb|IsaMakefile| is not made
-  part of the initial session directory created by \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}}).
-  See \verb|~~/src/HOL/IsaMakefile| for a full-blown example.%
+  part of the initial session directory created by \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}}).%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -430,18 +429,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Examples%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Refer to the \verb|IsaMakefile|s of the Isabelle
-  distribution's object-logics as a model for your own developments.
-  For example, see \verb|~~/src/FOL/IsaMakefile|.  The \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}} tool creates \verb|IsaMakefile|s with proper invocation
-  of \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} as well.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{Preparing Isabelle session documents
   \label{sec:tool-document}%
 }