diff -r f04b33ce250f -r a4dc62a46ee4 Makefile
--- 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