| changeset 9689 | 751fde5307e4 |
| parent 9666 | 3572fc1dbe6b |
| child 9721 | 7e51c9f3d5a0 |
--- a/doc-src/TutorialI/IsaMakefile Fri Aug 25 12:17:09 2000 +0200 +++ b/doc-src/TutorialI/IsaMakefile Mon Aug 28 09:32:51 2000 +0200 @@ -88,7 +88,7 @@ $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \ Recdef/simplification.thy Recdef/Induction.thy \ - Recdef/Nested0.thy Recdef/Nested1.thy + Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef @rm -f tutorial.dvi