src/HOLCF/IsaMakefile
changeset 27307 70c98cd37161
parent 26456 a63501938ce1
child 27400 42ee5e7c3b50
equal deleted inserted replaced
27306:0609faccb903 27307:70c98cd37161
    28 	@cd $(SRC)/HOL; $(ISATOOL) make HOL
    28 	@cd $(SRC)/HOL; $(ISATOOL) make HOL
    29 
    29 
    30 $(OUT)/HOLCF: $(OUT)/HOL Adm.thy Bifinite.thy Cfun.thy			\
    30 $(OUT)/HOLCF: $(OUT)/HOL Adm.thy Bifinite.thy Cfun.thy			\
    31   CompactBasis.thy Cont.thy ConvexPD.thy Cprod.thy Discrete.thy		\
    31   CompactBasis.thy Cont.thy ConvexPD.thy Cprod.thy Discrete.thy		\
    32   Domain.thy Ffun.thy Fixrec.thy Fix.thy HOLCF.thy Lift.thy		\
    32   Domain.thy Ffun.thy Fixrec.thy Fix.thy HOLCF.thy Lift.thy		\
    33   LowerPD.thy One.thy Pcpodef.thy Pcpo.thy Porder.thy SetPcpo.thy	\
    33   LowerPD.thy One.thy Pcpodef.thy Pcpo.thy Porder.thy Cset.thy		\
    34   Sprod.thy Ssum.thy Tr.thy UpperPD.thy Up.thy ROOT.ML			\
    34   Sprod.thy Ssum.thy Tr.thy UpperPD.thy Up.thy ROOT.ML			\
    35   Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML		\
    35   Tools/adm_tac.ML Tools/cont_consts.ML Tools/cont_proc.ML		\
    36   Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML		\
    36   Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML		\
    37   Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML		\
    37   Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML		\
    38   Tools/domain/domain_theorems.ML Tools/fixrec_package.ML		\
    38   Tools/domain/domain_theorems.ML Tools/fixrec_package.ML		\