*** empty log message ***
authornipkow
Mon, 21 Aug 2000 17:54:43 +0200
changeset 9666 3572fc1dbe6b
parent 9665 2a6d7f1409f9
child 9667 48cefe2daf32
*** empty log message ***
doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Mon Aug 21 13:47:24 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Mon Aug 21 17:54:43 2000 +0200
@@ -67,7 +67,7 @@
 HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
 
 $(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
-  Datatype/Nested.thy Datatype/Nested2.thy Datatype/unfoldnested.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