equal
deleted
inserted
replaced
43 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
43 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
44 |
44 |
45 test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES) |
45 test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES) |
46 @$(ISATOOL) testdir $(OUT)/HOLCF ex |
46 @$(ISATOOL) testdir $(OUT)/HOLCF ex |
47 |
47 |
48 |
|
49 ## Explicit domains |
|
50 # |
|
51 #EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy\ |
|
52 # explicit_domains/Dlist.thy \ |
|
53 # explicit_domains/Stream.thy explicit_domains/Stream2.thy |
|
54 |
|
55 #EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \ |
|
56 # $(EXPLICIT_DOMAINS_THYS:.thy=.ML) |
|
57 # |
|
58 #test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES) |
|
59 # @$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains |
|
60 |
|
61 |
|
62 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF |
48 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF |