doc-src/Ref/document/root.tex

 \documentclass[12pt,a4paper]{report}
 \usepackage{graphicx,iman,extra,ttbox,proof,pdfsetup}
 
-%%\includeonly{}
 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
 %%% to delete old ones:  \\indexbold{\*[^}]*}
 %% run    sedindex ref    to prepare index file
 %%% needs chapter on Provers/typedsimp.ML?
 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Isabelle Reference Manual}

   (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
   Schwerpunktprogramm \emph{Deduktion}.
 
 \pagenumbering{roman} \tableofcontents \clearfirst
 
-\include{tactic}
-\include{thm}
-\include{syntax}
-\include{substitution}
-\include{simplifier}
-\include{classical}
+\input{tactic}
+\input{thm}
+\input{syntax}
+\input{substitution}
+\input{simplifier}
+\input{classical}
 
 %%seealso's must be last so that they appear last in the index entries
 \index{meta-rewriting|seealso{tactics, theorems}}
 
 \begingroup
   \bibliographystyle{plain} \small\raggedright\frenchspacing
   \bibliography{manual}
 \endgroup
-\include{theory-syntax}
 
 \printindex
 \end{document}