--- a/Makefile Wed Jun 21 15:12:40 1995 +0200
+++ b/Makefile Thu Jun 29 12:29:58 1995 +0200
@@ -1,7 +1,7 @@
# $Id$
#########################################################################
# #
-# Makefile for Isabelle (HOL) #
+# Makefile for Isabelle (Old_HOL) #
# #
#########################################################################
@@ -29,17 +29,18 @@
../Provers/simplifier.ML ../Provers/splitter.ML\
$(NAMES:%=%.thy) $(NAMES:%=%.ML)
-$(BIN)/HOL: $(BIN)/Pure $(FILES)
+$(BIN)/Old_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();' \
+ poly*) echo 'make_database"$(BIN)/Old_HOL"; quit();' \
| $(COMP) $(BIN)/Pure;\
- echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/HOL ;;\
- sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure ;;\
+ echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/Old_HOL;;\
+ sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/Old_HOL" banner;' | \
+ $(BIN)/Pure ;;\
*) echo Bad value for ISABELLECOMP: \
$(COMP) is not poly or sml; exit 1;;\
esac
@@ -51,8 +52,8 @@
#A macro referring to the object-logic (depends on ML compiler)
LOGIC:sh=case $ISABELLECOMP in \
- poly*) echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
- sml*) echo "$ISABELLEBIN/HOL" ;;\
+ poly*) echo "$ISABELLECOMP $ISABELLEBIN/Old_HOL" ;;\
+ sml*) echo "$ISABELLEBIN/Old_HOL" ;;\
*) echo "echo Bad value for ISABELLECOMP: \
$ISABELLEBIN is not poly or sml; exit 1" ;;\
esac
@@ -61,7 +62,7 @@
IMP_NAMES = Com Denotation Equiv Properties
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
-IMP: $(BIN)/HOL $(IMP_FILES)
+IMP: $(BIN)/Old_HOL $(IMP_FILES)
echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
##The integers in HOL
@@ -70,7 +71,7 @@
INTEG_FILES = Integ/ROOT.ML \
$(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
-Integ: $(BIN)/HOL $(INTEG_FILES)
+Integ: $(BIN)/Old_HOL $(INTEG_FILES)
echo 'exit_use"Integ/ROOT.ML";quit();' | $(LOGIC)
##I/O Automata
@@ -81,7 +82,7 @@
$(IOA_EX_NAMES:%=IOA/example/%.thy) $(IOA_EX_NAMES:%=IOA/example/%.ML)\
$(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
-IOA: $(BIN)/HOL $(IOA_FILES)
+IOA: $(BIN)/Old_HOL $(IOA_FILES)
echo 'exit_use"IOA/ROOT.ML";quit();' | $(LOGIC)
##Properties of substitutions
@@ -90,7 +91,7 @@
SUBST_FILES = Subst/ROOT.ML \
$(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
-Subst: $(BIN)/HOL $(SUBST_FILES)
+Subst: $(BIN)/Old_HOL $(SUBST_FILES)
echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC)
##Miscellaneous examples
@@ -99,11 +100,11 @@
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
-ex: $(BIN)/HOL $(EX_FILES)
+ex: $(BIN)/Old_HOL $(EX_FILES)
echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
#Full test.
-test: $(BIN)/HOL IMP Integ IOA Subst ex
+test: $(BIN)/Old_HOL IMP Integ IOA Subst ex
echo 'Test examples ran successfully' > test
-.PRECIOUS: $(BIN)/Pure $(BIN)/HOL
+.PRECIOUS: $(BIN)/Pure $(BIN)/Old_HOL