# HG changeset patch
# User wenzelm
# Date 1346163503 -7200
# Node ID 8be091776e9310339f9ca396b290fb0a6a3a63fe
# Parent  6f7be3f5da94df9ae0788c7a8de52d78dc75cb5a
prefer \input which actually checks file existence;

diff -r 6f7be3f5da94 -r 8be091776e93 doc-src/HOL/document/root.tex
--- 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
diff -r 6f7be3f5da94 -r 8be091776e93 doc-src/Intro/document/root.tex
--- 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}
diff -r 6f7be3f5da94 -r 8be091776e93 doc-src/Logics/document/root.tex
--- 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
diff -r 6f7be3f5da94 -r 8be091776e93 doc-src/Ref/document/root.tex
--- 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}
diff -r 6f7be3f5da94 -r 8be091776e93 doc-src/ZF/document/root.tex
--- 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}