src/HOL/IsaMakefile
changeset 3195 dcb458d38724
parent 3125 3f0ab2c306f7
child 3218 44f01b718eab
     1.1 --- a/src/HOL/IsaMakefile	Thu May 15 12:53:12 1997 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu May 15 12:53:39 1997 +0200
     1.3 @@ -8,9 +8,9 @@
     1.4  
     1.5  OUT = $(ISABELLE_OUTPUT)
     1.6  
     1.7 -NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
     1.8 +NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
     1.9  	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
    1.10 -	Sexp Univ List RelPow Option
    1.11 +	Psubset Sexp Univ List RelPow Option
    1.12  
    1.13  FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
    1.14  	ind_syntax.ML cladata.ML simpdata.ML \
    1.15 @@ -28,17 +28,6 @@
    1.16  	@cd ../Pure; $(ISATOOL) make
    1.17  
    1.18  
    1.19 -## TFL (requires integration into HOL proper)
    1.20 -
    1.21 -TFL_NAMES = mask tfl thms thry usyntax utils
    1.22 -TFL_FILES = ../TFL/ROOT.ML ../TFL/sys.sml \
    1.23 -            $(TFL_NAMES:%=../TFL/%.sig) $(TFL_NAMES:%=../TFL/%.sml)
    1.24 -
    1.25 -TFL:	$(OUT)/HOL $(TFL_FILES)
    1.26 -	@$(ISABELLE) -qe 'exit_use_dir"../TFL"; quit();' HOL
    1.27 -
    1.28 -
    1.29 -
    1.30  #### Tests and examples
    1.31  
    1.32  ## Inductive definitions: simple examples
    1.33 @@ -105,7 +94,7 @@
    1.34  
    1.35  ## Properties of substitutions
    1.36  
    1.37 -SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
    1.38 +SUBST_NAMES = AList Subst Unifier UTerm Unify
    1.39  
    1.40  SUBST_FILES = Subst/ROOT.ML \
    1.41  	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
    1.42 @@ -208,7 +197,7 @@
    1.43  ## Full test
    1.44  
    1.45  test:	$(OUT)/HOL \
    1.46 -		TFL Induct IMP Hoare Lex Integ Auth Subst Lambda  \
    1.47 +		Subst Induct IMP Hoare Lex Integ Auth Lambda  \
    1.48  		W0 MiniML IOA AxClasses Quot ex
    1.49  	echo 'Test examples ran successfully' > test
    1.50