# HG changeset patch # User nipkow # Date 794679787 -3600 # Node ID 01d6571fa10643b176eb0fc9e8a501ad1a45f940 # Parent 8477483f663f8d4ab600ede2c27dde58a08e4e12 Added dependencies on ../Provers/hypsubst.ML and removed those on ../Provers/ind.ML diff -r 8477483f663f -r 01d6571fa106 src/HOL/Makefile --- a/src/HOL/Makefile Wed Mar 08 14:35:26 1995 +0100 +++ b/src/HOL/Makefile Wed Mar 08 17:23:07 1995 +0100 @@ -26,8 +26,9 @@ 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/classical.ML ../Provers/simplifier.ML \ - ../Provers/splitter.ML ../Provers/ind.ML $(THYS) $(THYS:.thy=.ML) + ../Provers/hypsubst.ML ../Provers/classical.ML\ + ../Provers/simplifier.ML ../Provers/splitter.ML\ + $(THYS) $(THYS:.thy=.ML) $(BIN)/CHOL: $(BIN)/Pure $(FILES) if [ -d $${ISABELLEBIN:?}/Pure ];\