Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Types chapter now uses HOL-Real
authorpaulson
Wed, 03 Jan 2001 11:13:51 +0100
changeset 10765 94aa0b568009
parent 10764 329d5f4aa43c
child 10766 ace2ba2d4fd1
Types chapter now uses HOL-Real
doc-src/TutorialI/IsaMakefile file | annotate | diff | comparison | revisions 
--- a/doc-src/TutorialI/IsaMakefile	Wed Jan 03 11:13:13 2001 +0100
+++ b/doc-src/TutorialI/IsaMakefile	Wed Jan 03 11:13:51 2001 +0100
@@ -16,12 +16,16 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 USEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL
+REALUSEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL-Real
 
 ## HOL
 
 HOL:
 	@cd $(SRC)/HOL; $(ISATOOL) make HOL
 
+HOL-Real:
+	@cd $(SRC)/HOL; $(ISATOOL) make HOL-Real
+
 styles:
 	@rm -f isabelle.sty
 	@rm -f isabellesym.sty
@@ -145,13 +149,13 @@
 
 ## HOL-Types
 
-HOL-Types: HOL $(LOG)/HOL-Types.gz
+HOL-Types: HOL-Real $(LOG)/HOL-Types.gz
 
-$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
+$(LOG)/HOL-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \
   Types/Numbers.thy Types/Pairs.thy Types/Typedef.thy \
   Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
   Types/Overloading.thy Types/Axioms.thy
-	$(USEDIR) Types
+	$(REALUSEDIR) Types
 	@rm -f tutorial.dvi
 
 ## HOL-Misc
isabelle