30 |
30 |
31 #### Tests and examples |
31 #### Tests and examples |
32 |
32 |
33 ## Miscellaneous examples |
33 ## Miscellaneous examples |
34 |
34 |
35 EX_THYS = ex/Fix2.thy ex/Hoare.thy \ |
35 EX_THYS = ex/Classlib.thy ex/Witness.thy\ |
36 ex/Loop.thy |
36 ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\ |
|
37 ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\ |
|
38 ex/Hoare.thy ex/Loop.thy |
37 |
39 |
38 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
40 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
39 |
41 |
40 test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES) |
42 test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES) |
41 @$(ISATOOL) testdir $(OUT)/HOLCF ex |
43 @$(ISATOOL) testdir $(OUT)/HOLCF ex |
42 |
44 |
43 |
45 |
44 ## Explicit domains |
46 ## Explicit domains |
|
47 # |
|
48 #EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy\ |
|
49 # explicit_domains/Dlist.thy \ |
|
50 # explicit_domains/Stream.thy explicit_domains/Stream2.thy |
45 |
51 |
46 EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \ |
52 #EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \ |
47 explicit_domains/Dnat2.thy explicit_domains/Stream.thy \ |
53 # $(EXPLICIT_DOMAINS_THYS:.thy=.ML) |
48 explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy \ |
54 # |
49 explicit_domains/Focus_ex.thy explicit_domains/Stream2.thy |
55 #test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES) |
50 |
56 # @$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains |
51 EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \ |
|
52 $(EXPLICIT_DOMAINS_THYS:.thy=.ML) |
|
53 |
|
54 test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES) |
|
55 @$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains |
|
56 |
57 |
57 |
58 |
58 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF |
59 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF |