doc-src/Ref/document/root.tex
changeset 48970 8be091776e93
parent 48939 83bd9eb1c70c
--- a/doc-src/Ref/document/root.tex	Tue Aug 28 16:14:35 2012 +0200
+++ b/doc-src/Ref/document/root.tex	Tue Aug 28 16:18:23 2012 +0200
@@ -1,7 +1,6 @@
 \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
@@ -47,12 +46,12 @@
 
 \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}}
@@ -61,7 +60,6 @@
   \bibliographystyle{plain} \small\raggedright\frenchspacing
   \bibliography{manual}
 \endgroup
-\include{theory-syntax}
 
 \printindex
 \end{document}