58 esac |
58 esac |
59 |
59 |
60 $(BIN)/HOL: |
60 $(BIN)/HOL: |
61 cd ../HOL; $(MAKE) |
61 cd ../HOL; $(MAKE) |
62 |
62 |
63 EX_THYS = ex/Fix2.thy ex/Hoare.thy \ |
63 EX_THYS = ex/Classlib.thy ex/Witness.thy\ |
64 ex/Loop.thy |
64 ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\ |
|
65 ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\ |
|
66 ex/Hoare.thy ex/Loop.thy |
65 |
67 |
66 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
68 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
67 |
69 |
68 test: ex/ROOT.ML $(BIN)/HOLCF $(EX_FILES) |
70 test: ex/ROOT.ML $(BIN)/HOLCF $(EX_FILES) |
69 @case `basename "$(COMP)"` in \ |
71 @case `basename "$(COMP)"` in \ |
79 fi;;\ |
81 fi;;\ |
80 *) echo Bad value for ISABELLECOMP: \ |
82 *) echo Bad value for ISABELLECOMP: \ |
81 \"$(COMP)\" is not poly or sml;;\ |
83 \"$(COMP)\" is not poly or sml;;\ |
82 esac |
84 esac |
83 |
85 |
84 EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \ |
86 #EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy \ |
85 explicit_domains/Dnat2.thy explicit_domains/Stream.thy \ |
87 # explicit_domains/Dlist.thy \ |
86 explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy\ |
88 # explicit_domains/Stream.thy explicit_domains/Stream2.thy |
87 explicit_domains/Focus_ex.thy explicit_domains/Stream2.thy |
|
88 |
89 |
89 EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\ |
90 #EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\ |
90 $(EXPLICIT_DOMAINS_THYS:.thy=.ML) |
91 # $(EXPLICIT_DOMAINS_THYS:.thy=.ML) |
91 |
92 |
92 test2: explicit_domains/ROOT.ML $(BIN)/HOLCF $(EXPLICIT_DOMAINS_FILES) |
93 #test2: explicit_domains/ROOT.ML $(BIN)/HOLCF $(EXPLICIT_DOMAINS_FILES) |
93 @case `basename "$(COMP)"` in \ |
94 # @case `basename "$(COMP)"` in \ |
94 poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
95 # poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
95 then echo 'make_html := true; exit_use_dir"explicit_domains"; quit();' | $(COMP) $(BIN)/HOLCF;\ |
96 # then echo 'make_html := true; exit_use_dir"explicit_domains";\ |
96 else echo 'exit_use_dir"explicit_domains"; quit();' \ |
97 # quit();' | $(COMP) $(BIN)/HOLCF;\ |
97 | $(COMP) $(BIN)/HOLCF;\ |
98 # else echo 'exit_use_dir"explicit_domains"; quit();' \ |
98 fi;;\ |
99 # | $(COMP) $(BIN)/HOLCF;\ |
99 sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
100 # fi;;\ |
100 then echo 'make_html := true; exit_use_dir"exlicit_domains";' \ |
101 # sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
101 | $(BIN)/HOLCF;\ |
102 # then echo 'make_html := true; exit_use_dir"exlicit_domains";' \ |
102 else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\ |
103 # | $(BIN)/HOLCF;\ |
103 fi;;\ |
104 # else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\ |
104 *) echo Bad value for ISABELLECOMP: \ |
105 # fi;;\ |
105 \"$(COMP)\" is not poly or sml;;\ |
106 # *) echo Bad value for ISABELLECOMP: \ |
106 esac |
107 # \"$(COMP)\" is not poly or sml;;\ |
|
108 # esac |
107 |
109 |
108 .PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF |
110 .PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF |
109 |
111 |