4 # IsaMakefile for HOLCF
9 OUT = $(ISABELLE_OUTPUT_DIR)
11 THYS = Void.thy Porder.thy Pcpo.thy \
12 Fun1.thy Fun2.thy Fun3.thy \
13 Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
14 Cprod1.thy Cprod2.thy Cprod3.thy \
15 Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
16 Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
17 Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy One.thy \
18 Tr1.thy Tr2.thy Lift1.thy Lift2.thy Lift2.thy HOLCF.thy
20 FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML)
22 $(OUT)/HOLCF: $(OUT)/HOL $(FILES)
23 @$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/HOL HOLCF
27 @cd ../HOL; $(ISATOOL) make
31 #### Tests and examples
33 ## Miscellaneous examples
35 EX_THYS = ex/Fix2.thy ex/Hoare.thy \
38 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
40 test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES)
41 @$(ISATOOL) testdir $(OUT)/HOLCF ex
46 EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \
47 explicit_domains/Dnat2.thy explicit_domains/Stream.thy \
48 explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy \
49 explicit_domains/Focus_ex.thy explicit_domains/Stream2.thy
51 EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \
52 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
54 test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES)
55 @$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains
58 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF