--- a/doc-src/HOL/document/root.tex Tue Aug 28 16:14:35 2012 +0200
+++ b/doc-src/HOL/document/root.tex Tue Aug 28 16:18:23 2012 +0200
@@ -53,7 +53,7 @@
\pagenumbering{roman} \tableofcontents \clearfirst
\input{syntax}
-\include{HOL}
+\input{HOL}
\bibliographystyle{plain}
\bibliography{manual}
\printindex
--- a/doc-src/Intro/document/root.tex Tue Aug 28 16:14:35 2012 +0200
+++ b/doc-src/Intro/document/root.tex Tue Aug 28 16:18:23 2012 +0200
@@ -143,9 +143,9 @@
\end{quote}
\clearfirst \pagestyle{headings}
-\include{foundations}
-\include{getting}
-\include{advanced}
+\input{foundations}
+\input{getting}
+\input{advanced}
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{manual}
--- a/doc-src/Logics/document/root.tex Tue Aug 28 16:14:35 2012 +0200
+++ b/doc-src/Logics/document/root.tex Tue Aug 28 16:18:23 2012 +0200
@@ -39,12 +39,12 @@
\begin{document}
\maketitle
\pagenumbering{roman} \tableofcontents \clearfirst
-\include{preface}
-\include{syntax}
-\include{LK}
-\include{Sequents}
-%%\include{Modal}
-\include{CTT}
+\input{preface}
+\input{syntax}
+\input{LK}
+\input{Sequents}
+%%\input{Modal}
+\input{CTT}
\bibliographystyle{plain}
\bibliography{manual}
\printindex
--- 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}
--- a/doc-src/ZF/document/root.tex Tue Aug 28 16:14:35 2012 +0200
+++ b/doc-src/ZF/document/root.tex Tue Aug 28 16:18:23 2012 +0200
@@ -78,11 +78,11 @@
\pagenumbering{arabic}
\setcounter{page}{1}
\input{syntax}
-\include{FOL}
-\include{ZF}
+\input{FOL}
+\input{ZF}
\isabellestyle{literal}
-\include{ZF_Isar}
+\input{ZF_Isar}
\isabellestyle{tt}
\bibliographystyle{plain}