isabelle: src/HOLCF/IsaMakefile@59bd96046ad6 (annotated)

2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	1	#
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	2	# $Id$
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	3	#
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	4	# IsaMakefile for HOLCF
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	5	#
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	6
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	7	#### Base system
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	8
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	9	OUT = $(ISABELLE_OUTPUT_DIR)
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	10
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2571 diff changeset	11	THYS = Porder.thy Porder0.thy Pcpo.thy \
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	12	Fun1.thy Fun2.thy Fun3.thy \
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	13	Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	14	Cprod1.thy Cprod2.thy Cprod3.thy \
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	15	Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	16	Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2571 diff changeset	17	Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2571 diff changeset	18	One.thy Tr.thy\
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2571 diff changeset	19	Lift1.thy Lift2.thy Lift3.thy HOLCF.thy
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	20
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2571 diff changeset	21	ONLYTHYS = Lift.thy
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2571 diff changeset	22
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2571 diff changeset	23	FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML)
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	24
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	25	$(OUT)/HOLCF: $(OUT)/HOL $(FILES)
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	26	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/HOL HOLCF
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	27	@chmod -w $@
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	28
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	29	$(OUT)/HOL:
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	30	@cd ../HOL; $(ISATOOL) make
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	31
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	32
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	33
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	34	#### Tests and examples
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	35
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	36	## Miscellaneous examples
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	37
2571 b9f641195b48 reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains oheimb parents: 2494 diff changeset	38	EX_THYS = ex/Classlib.thy ex/Witness.thy\
b9f641195b48 reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains oheimb parents: 2494 diff changeset	39	ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\
b9f641195b48 reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains oheimb parents: 2494 diff changeset	40	ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\
b9f641195b48 reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains oheimb parents: 2494 diff changeset	41	ex/Hoare.thy ex/Loop.thy
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	42
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	43	EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	44
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	45	test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES)
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	46	@$(ISATOOL) testdir $(OUT)/HOLCF ex
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	47
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	48	.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF

author	wenzelm
	Fri, 07 Mar 1997 11:48:46 +0100
changeset 2754	59bd96046ad6
parent 2679	3eac428cdd1b
child 2797	54ca927b831b
permissions	-rw-r--r--