src/HOL/IsaMakefile
changeset 4864 3abfe2093aa0
parent 4830 bd73675adbed
child 4896 4727272f3db6
equal deleted inserted replaced
4863:d29776582f8c 4864:3abfe2093aa0
    41   $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \
    41   $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \
    42   Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy \
    42   Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy \
    43   Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.ML \
    43   Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.ML \
    44   Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \
    44   Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \
    45   Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
    45   Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
    46   Power.ML Power.thy Prod.ML Prod.thy ROOT.ML RelPow.ML RelPow.thy \
    46   Power.ML Power.thy Prod.ML Prod.thy Record.thy ROOT.ML RelPow.ML \
    47   Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy Sum.ML \
    47   RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
    48   Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy \
    48   Sum.ML Sum.thy Tools/record_package.ML Tools/typedef_package.ML \
    49   WF.ML WF.thy WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML \
    49   Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML \
    50   cladata.ML datatype.ML equalities.ML equalities.thy hologic.ML \
    50   WF.thy WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML cladata.ML \
    51   ind_syntax.ML indrule.ML indrule.thy intr_elim.ML intr_elim.thy \
    51   datatype.ML equalities.ML equalities.thy hologic.ML ind_syntax.ML \
    52   mono.ML mono.thy record.ML simpdata.ML subset.ML subset.thy \
    52   indrule.ML indrule.thy intr_elim.ML intr_elim.thy mono.ML mono.thy \
    53   thy_data.ML thy_syntax.ML typedef.ML
    53   simpdata.ML subset.ML subset.thy thy_data.ML thy_syntax.ML
    54 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    54 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    55 
    55 
    56 
    56 
    57 ## HOL-Subst
    57 ## HOL-Subst
    58 
    58