# HG changeset patch
# User wenzelm
# Date 852732764 -3600
# Node ID 5d45c2094ff622954afb64514b9818488c67de3a
# Parent  bdeb5024353af23079174b05f7c0e8bcab5ae014
IsaMakefile for HOLCF;

diff -r bdeb5024353a -r 5d45c2094ff6 src/HOLCF/IsaMakefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IsaMakefile	Wed Jan 08 15:12:44 1997 +0100
@@ -0,0 +1,58 @@
+#
+# $Id$
+#
+# IsaMakefile for HOLCF
+#
+
+#### Base system
+
+OUT = $(ISABELLE_OUTPUT_DIR)
+
+THYS = Void.thy Porder.thy Pcpo.thy \
+       Fun1.thy Fun2.thy Fun3.thy \
+       Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
+       Cprod1.thy Cprod2.thy Cprod3.thy \
+       Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
+       Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
+       Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy One.thy \
+       Tr1.thy Tr2.thy Lift1.thy Lift2.thy Lift2.thy HOLCF.thy
+
+FILES = ROOT.ML Porder0.thy  $(THYS) $(THYS:.thy=.ML)
+
+$(OUT)/HOLCF: $(OUT)/HOL $(FILES)
+	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/HOL HOLCF
+	@chmod -w $@
+
+$(OUT)/HOL:
+	@cd ../HOL; $(ISATOOL) make
+
+
+
+#### Tests and examples
+
+## Miscellaneous examples
+
+EX_THYS = ex/Fix2.thy ex/Hoare.thy \
+	  ex/Loop.thy
+
+EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
+
+test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES)
+	@$(ISATOOL) testdir $(OUT)/HOLCF ex
+
+
+## Explicit domains
+
+EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \
+			explicit_domains/Dnat2.thy explicit_domains/Stream.thy \
+			explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy \
+			explicit_domains/Focus_ex.thy explicit_domains/Stream2.thy
+
+EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \
+			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
+
+test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES)
+	@$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains
+
+
+.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF