diff -r c452fea3ce74 -r 499637e8f2c6 doc-src/TutorialI/IsaMakefile --- a/doc-src/TutorialI/IsaMakefile Wed Oct 11 00:03:22 2000 +0200 +++ b/doc-src/TutorialI/IsaMakefile Wed Oct 11 09:09:06 2000 +0200 @@ -87,9 +87,9 @@ HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz -$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \ +$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \ Recdef/simplification.thy Recdef/Induction.thy \ - Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy + Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy Recdef/WFrec.thy @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef @rm -f tutorial.dvi