--- a/doc-src/TutorialI/IsaMakefile Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/IsaMakefile Thu Nov 01 20:20:19 2007 +0100
@@ -4,7 +4,7 @@
## targets
-default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef \
+default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Recdef \
HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Complex-Types HOL-Misc \
HOL-Protocol HOL-Documents styles
images:
@@ -95,6 +95,15 @@
@rm -f tutorial.dvi
+## HOL-Fun
+
+HOL-Fun: HOL $(LOG)/HOL-Fun.gz
+
+$(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy
+ $(USEDIR) Fun
+ @rm -f tutorial.dvi
+
+
## HOL-Recdef
HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz