Types chapter now uses HOL-Real
authorpaulson
Wed Jan 03 11:13:51 2001 +0100 (2001-01-03)
changeset 1076594aa0b568009
parent 10764 329d5f4aa43c
child 10766 ace2ba2d4fd1
Types chapter now uses HOL-Real
doc-src/TutorialI/IsaMakefile
     1.1 --- a/doc-src/TutorialI/IsaMakefile	Wed Jan 03 11:13:13 2001 +0100
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Wed Jan 03 11:13:51 2001 +0100
     1.3 @@ -16,12 +16,16 @@
     1.4  OUT = $(ISABELLE_OUTPUT)
     1.5  LOG = $(OUT)/log
     1.6  USEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL
     1.7 +REALUSEDIR = @$(ISATOOL) usedir -m brackets -i true -d dvi -D document $(OUT)/HOL-Real
     1.8  
     1.9  ## HOL
    1.10  
    1.11  HOL:
    1.12  	@cd $(SRC)/HOL; $(ISATOOL) make HOL
    1.13  
    1.14 +HOL-Real:
    1.15 +	@cd $(SRC)/HOL; $(ISATOOL) make HOL-Real
    1.16 +
    1.17  styles:
    1.18  	@rm -f isabelle.sty
    1.19  	@rm -f isabellesym.sty
    1.20 @@ -145,13 +149,13 @@
    1.21  
    1.22  ## HOL-Types
    1.23  
    1.24 -HOL-Types: HOL $(LOG)/HOL-Types.gz
    1.25 +HOL-Types: HOL-Real $(LOG)/HOL-Types.gz
    1.26  
    1.27 -$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
    1.28 +$(LOG)/HOL-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \
    1.29    Types/Numbers.thy Types/Pairs.thy Types/Typedef.thy \
    1.30    Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
    1.31    Types/Overloading.thy Types/Axioms.thy
    1.32 -	$(USEDIR) Types
    1.33 +	$(REALUSEDIR) Types
    1.34  	@rm -f tutorial.dvi
    1.35  
    1.36  ## HOL-Misc