got rid of separate root.tex;

--- a/doc-src/TutorialI/Advanced/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/CTL/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/CodeGen/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/Datatype/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/Documents/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/Ifexpr/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/Inductive/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/IsaMakefile	Sat Oct 20 20:23:37 2001 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Sat Oct 20 22:07:44 2001 +0200
@@ -17,7 +17,7 @@
 SRC = $(ISABELLE_HOME)/src
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
-OPTIONS = -m brackets -i true -d dvi -D document
+OPTIONS = -m brackets -i true -d "" -D document
 USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL
 REALUSEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL-Real
 

--- a/doc-src/TutorialI/Misc/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/Recdef/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/Rules/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/Sets/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/ToyList/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/Trie/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}

--- a/doc-src/TutorialI/Types/document/root.tex	Sat Oct 20 20:23:37 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\documentclass{article}
-\begin{document}
-xxx
-\end{document}