--- a/doc-src/TutorialI/IsaMakefile Fri Dec 21 17:31:45 2001 +0100
+++ b/doc-src/TutorialI/IsaMakefile Fri Dec 21 19:55:39 2001 +0100
@@ -169,7 +169,7 @@
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \
- Misc/types.thy Misc/prime_def.thy Misc/Translations.thy Misc/case_exprs.thy \
+ Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
$(USEDIR) Misc
@rm -f tutorial.dvi