# HG changeset patch # User paulson # Date 978516831 -3600 # Node ID 94aa0b568009517ae1f44a5865e9f65f4fe444bb # Parent 329d5f4aa43cc1098f63c4db52c9ccaf2bb58ee1 Types chapter now uses HOL-Real diff -r 329d5f4aa43c -r 94aa0b568009 doc-src/TutorialI/IsaMakefile --- 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