author | oheimb |
Fri, 31 Jan 1997 16:57:45 +0100 | |
changeset 2571 | b9f641195b48 |
parent 2494 | 5d45c2094ff6 |
child 2640 | ee4dfce170a0 |
permissions | -rw-r--r-- |
2494 | 1 |
# |
2 |
# $Id$ |
|
3 |
# |
|
4 |
# IsaMakefile for HOLCF |
|
5 |
# |
|
6 |
||
7 |
#### Base system |
|
8 |
||
9 |
OUT = $(ISABELLE_OUTPUT_DIR) |
|
10 |
||
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 |
|
19 |
||
20 |
FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML) |
|
21 |
||
22 |
$(OUT)/HOLCF: $(OUT)/HOL $(FILES) |
|
23 |
@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/HOL HOLCF |
|
24 |
@chmod -w $@ |
|
25 |
||
26 |
$(OUT)/HOL: |
|
27 |
@cd ../HOL; $(ISATOOL) make |
|
28 |
||
29 |
||
30 |
||
31 |
#### Tests and examples |
|
32 |
||
33 |
## Miscellaneous examples |
|
34 |
||
2571
b9f641195b48
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
oheimb
parents:
2494
diff
changeset
|
35 |
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
|
36 |
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
|
37 |
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
|
38 |
ex/Hoare.thy ex/Loop.thy |
2494 | 39 |
|
40 |
EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
|
41 |
||
42 |
test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES) |
|
43 |
@$(ISATOOL) testdir $(OUT)/HOLCF ex |
|
44 |
||
45 |
||
46 |
## Explicit domains |
|
2571
b9f641195b48
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
oheimb
parents:
2494
diff
changeset
|
47 |
# |
b9f641195b48
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
oheimb
parents:
2494
diff
changeset
|
48 |
#EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy\ |
b9f641195b48
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
oheimb
parents:
2494
diff
changeset
|
49 |
# explicit_domains/Dlist.thy \ |
b9f641195b48
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
oheimb
parents:
2494
diff
changeset
|
50 |
# explicit_domains/Stream.thy explicit_domains/Stream2.thy |
2494 | 51 |
|
2571
b9f641195b48
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
oheimb
parents:
2494
diff
changeset
|
52 |
#EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \ |
b9f641195b48
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
oheimb
parents:
2494
diff
changeset
|
53 |
# $(EXPLICIT_DOMAINS_THYS:.thy=.ML) |
b9f641195b48
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
oheimb
parents:
2494
diff
changeset
|
54 |
# |
b9f641195b48
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
oheimb
parents:
2494
diff
changeset
|
55 |
#test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES) |
b9f641195b48
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
oheimb
parents:
2494
diff
changeset
|
56 |
# @$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains |
2494 | 57 |
|
58 |
||
59 |
.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF |