# HG changeset patch
# User wenzelm
# Date 1003608464 -7200
# Node ID cc3d971fe66ae895cfe72622e5aa2458d552c819
# Parent  a35af478aee4eb6e03af9270f2ab04751c272eca
got rid of separate root.tex;

diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/Advanced/document/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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/CTL/document/root.tex
--- 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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/CodeGen/document/root.tex
--- 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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/Datatype/document/root.tex
--- 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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/Documents/document/root.tex
--- 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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/Ifexpr/document/root.tex
--- 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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/Inductive/document/root.tex
--- 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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/IsaMakefile
--- 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
 
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/Misc/document/root.tex
--- 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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/Recdef/document/root.tex
--- 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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/Rules/document/root.tex
--- 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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/Sets/document/root.tex
--- 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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/ToyList/document/root.tex
--- 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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/Trie/document/root.tex
--- 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}
diff -r a35af478aee4 -r cc3d971fe66a doc-src/TutorialI/Types/document/root.tex
--- 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}