--- a/Makefile Wed May 25 13:03:19 1994 +0200
+++ b/Makefile Wed Jun 01 13:24:54 1994 +0200
@@ -21,8 +21,9 @@
FILES = ROOT.ML HOL.thy HOL.ML simpdata.ML Ord.thy Ord.ML \
fun.ML Set.thy Set.ML subset.ML equalities.ML \
Prod.thy Prod.ML Sum.thy Sum.ML WF.thy WF.ML \
- mono.ML Lfp.thy Lfp.ML Gfp.thy Gfp.ML Nat.thy Nat.ML Sexp.thy \
- Sexp.ML Univ.thy Univ.ML LList.thy LList.ML List.thy List.ML \
+ mono.ML Lfp.thy Lfp.ML Gfp.thy Gfp.ML Nat.thy Nat.ML \
+ Arith.thy Arith.ML Sexp.thy Sexp.ML Univ.thy Univ.ML \
+ LList.thy LList.ML List.thy List.ML \
Datatype.ML \
../Provers/classical.ML ../Provers/simplifier.ML \
../Provers/splitter.ML ../Provers/ind.ML
@@ -42,12 +43,18 @@
Subst/UTLemmas.ML Subst/UTLemmas.thy
$(BIN)/HOL: $(BIN)/Pure $(FILES)
+ if [ -d $${ISABELLEBIN:?}/Pure ];\
+ then echo Bad value for ISABELLEBIN: \
+ $(BIN) is the Isabelle source directory; \
+ exit 1; \
+ fi;\
case "$(COMP)" in \
poly*) echo 'make_database"$(BIN)/HOL"; quit();' \
| $(COMP) $(BIN)/Pure;\
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/HOL ;;\
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure ;;\
- *) echo Bad value for ISABELLECOMP;;\
+ *) echo Bad value for ISABELLECOMP: \
+ $(COMP) is not poly or sml;;\
esac
$(BIN)/Pure:
@@ -58,7 +65,8 @@
poly*) echo 'use"ex/ROOT.ML"; use"Subst/ROOT.ML"; quit();' \
| $(COMP) $(BIN)/HOL ;;\
sml*) echo 'use"ex/ROOT.ML";use"Subst/ROOT.ML";' | $(BIN)/HOL;;\
- *) echo Bad value for ISABELLECOMP;;\
+ *) echo Bad value for ISABELLECOMP: \
+ $(COMP) is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/Pure $(BIN)/HOL