src/HOL/IsaMakefile
changeset 3232 19a2b853ba7b
parent 3222 726a9b069947
child 3294 4c73b6508f53
     1.1 --- a/src/HOL/IsaMakefile	Tue May 20 11:33:02 1997 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue May 20 11:33:45 1997 +0200
     1.3 @@ -12,13 +12,18 @@
     1.4  	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
     1.5  	Sexp Univ List RelPow Option
     1.6  
     1.7 +PROVERS = hypsubst.ML classical.ML blast.ML \
     1.8 +	simplifier.ML splitter.ML nat_transitive.ML 
     1.9 +
    1.10 +TFL   = dcterm.sml mask.sig mask.sml post.sml rules.new.sml rules.sig \
    1.11 +	sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml   \
    1.12 +	usyntax.sig usyntax.sml utils.sig utils.sml
    1.13 +
    1.14  FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
    1.15  	ind_syntax.ML cladata.ML simpdata.ML \
    1.16  	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \
    1.17 -	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
    1.18 -	../Provers/simplifier.ML ../Provers/splitter.ML \
    1.19 -	../Provers/nat_transitive.ML \
    1.20 -	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    1.21 +	$(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \
    1.22 +	$(PROVERS:%=../Provers/%)
    1.23  
    1.24  $(OUT)/HOL: $(OUT)/Pure $(FILES)
    1.25  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    1.26 @@ -195,7 +200,7 @@
    1.27  
    1.28  ## Miscellaneous examples
    1.29  
    1.30 -EX_NAMES = String BT InSort Qsort LexProd Puzzle Primes NatSum MT
    1.31 +EX_NAMES = String BT InSort Qsort Puzzle Primes NatSum MT
    1.32  
    1.33  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
    1.34  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)