--- a/doc-src/TutorialI/IsaMakefile Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile Fri Aug 18 10:34:08 2000 +0200
@@ -67,7 +67,8 @@
HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
- Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy
+ Datatype/Nested.thy Datatype/Nested2.thy Datatype/unfoldnested.thy \
+ Datatype/Fundata.thy
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype
@rm -f tutorial.dvi
@@ -86,7 +87,8 @@
HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \
- Recdef/simplification.thy Recdef/Induction.thy
+ Recdef/simplification.thy Recdef/Induction.thy \
+ Recdef/Nested0.thy Recdef/Nested1.thy
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef
@rm -f tutorial.dvi
@@ -99,7 +101,7 @@
Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.thy \
Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \
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
+ Misc/trace_simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/asm_simp.thy
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
@rm -f tutorial.dvi