--- a/Makefile Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,118 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (Old_HOL) #
-# #
-#########################################################################
-
-#To make the system, cd to this directory and type
-# make
-#To make the system and test it on standard examples, type
-# make test
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes pure Isabelle (Pure) if this file is ABSENT -- but not
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-NAMES = HOL Ord Set Fun subset equalities Prod Trancl Sum WF \
- mono Lfp Gfp Nat Inductive Finite Arith Sexp Univ List
-
-FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
- ind_syntax.ML indrule.ML intr_elim.ML simpdata.ML\
- subtype.ML thy_syntax.ML ../Pure/section_utils.ML\
- ../Provers/hypsubst.ML ../Provers/classical.ML\
- ../Provers/simplifier.ML ../Provers/splitter.ML\
- $(NAMES:%=%.thy) $(NAMES:%=%.ML)
-
-$(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)/Old_HOL"; quit();' \
- | $(COMP) $(BIN)/Pure;\
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
- then echo 'open PolyML; init_html (); exit_use"ROOT";' \
- | $(COMP) $(BIN)/Old_HOL;\
- else echo 'open PolyML; exit_use"ROOT";' \
- | $(COMP) $(BIN)/Old_HOL;\
- fi;;\
- sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
- then echo 'init_html (); exit_use"ROOT.ML"; xML"$(BIN)/Old_HOL" banner;' | $(BIN)/Pure;\
- else echo 'exit_use"ROOT.ML"; xML"$(BIN)/Old_HOL" banner;' \
- | $(BIN)/Pure;\
- fi;;\
- *) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml; exit 1;;\
- esac
-
-$(BIN)/Pure:
- cd ../Pure; $(MAKE)
-
-#### Testing of HOL
-
-#A macro referring to the object-logic (depends on ML compiler)
-LOGIC:sh=case $ISABELLECOMP in \
- 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
-
-##IMP-semantics example
-IMP_NAMES = Com Denotation Equiv Properties
-IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
-
-IMP: $(BIN)/Old_HOL $(IMP_FILES)
- echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
-
-##The integers in HOL
-INTEG_NAMES = Relation Equiv Integ
-
-INTEG_FILES = Integ/ROOT.ML \
- $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
-
-Integ: $(BIN)/Old_HOL $(INTEG_FILES)
- echo 'exit_use"Integ/ROOT.ML";quit();' | $(LOGIC)
-
-##I/O Automata
-IOA_EX_NAMES = Action Channels Correctness Impl Lemmas Multiset Receiver Sender
-IOA_MT_NAMES = Asig IOA Option Solve
-
-IOA_FILES = IOA/ROOT.ML IOA/example/Packet.thy IOA/example/Spec.thy\
- $(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)/Old_HOL $(IOA_FILES)
- echo 'exit_use"IOA/ROOT.ML";quit();' | $(LOGIC)
-
-##Properties of substitutions
-SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
-
-SUBST_FILES = Subst/ROOT.ML \
- $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
-
-Subst: $(BIN)/Old_HOL $(SUBST_FILES)
- echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC)
-
-##Miscellaneous examples
-EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String
-
-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)/Old_HOL $(EX_FILES)
- echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
-
-#Full test.
-test: $(BIN)/Old_HOL IMP Integ IOA Subst ex
- echo 'Test examples ran successfully' > test
-
-.PRECIOUS: $(BIN)/Pure $(BIN)/Old_HOL