# HG changeset patch
# User nipkow
# Date 956217296 -7200
# Node ID 42ce93ada11e79906d1631c5f48cfe899dee6e2a
# Parent  99511c569e0ad7733470119c2ebeefb77f3daea0
*** empty log message ***

diff -r 99511c569e0a -r 42ce93ada11e doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Wed Apr 19 15:27:08 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Thu Apr 20 09:54:56 2000 +0200
@@ -37,7 +37,7 @@
 
 $(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Ifexpr
-
+	@rm -f tutorial.dvi
 
 ## HOL-ToyList
 
@@ -48,9 +48,11 @@
 
 $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList2
+	@rm -f tutorial.dvi
 
 $(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList
+	@rm -f tutorial.dvi
 
 ## HOL-CodeGen
 
@@ -58,6 +60,7 @@
 
 $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CodeGen
+	@rm -f tutorial.dvi
 
 
 ## HOL-Datatype
@@ -67,6 +70,7 @@
 $(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
   Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype
+	@rm -f tutorial.dvi
 
 
 ## HOL-Trie
@@ -75,6 +79,7 @@
 
 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/Option2.thy Trie/Trie.thy
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Trie
+	@rm -f tutorial.dvi
 
 
 ## HOL-Recdef
@@ -84,6 +89,7 @@
 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \
   Recdef/simplification.thy Recdef/Induction.thy
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef
+	@rm -f tutorial.dvi
 
 
 ## HOL-Misc
@@ -96,9 +102,10 @@
   Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \
   Misc/trace_simp.thy Misc/Itrev.thy Misc/asm_simp.thy
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
+	@rm -f tutorial.dvi
 
 
 ## clean
 
 clean:
-	@rm -f $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz
+	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz
diff -r 99511c569e0a -r 42ce93ada11e doc-src/TutorialI/Makefile
--- a/doc-src/TutorialI/Makefile	Wed Apr 19 15:27:08 2000 +0200
+++ b/doc-src/TutorialI/Makefile	Thu Apr 20 09:54:56 2000 +0200
@@ -13,7 +13,8 @@
 
 NAME = tutorial
 FILES = tutorial.tex basics.tex fp.tex appendix.tex \
-	../iman.sty ttbox.sty extra.sty
+	../iman.sty ttbox.sty extra.sty \
+	isabelle.sty isabellesym.sty pdfsetup.sty
 
 dvi: $(NAME).dvi