# HG changeset patch
# User wenzelm
# Date 852731919 -3600
# Node ID 82f105e8a0f93ef90f8f46085ed60ad690f3a1ab
# Parent  55e940d84cdc906481380fcb5116c2b2fc14295e
IsaMakefile for CTT;

diff -r 55e940d84cdc -r 82f105e8a0f9 src/CTT/IsaMakefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/IsaMakefile	Wed Jan 08 14:58:39 1997 +0100
@@ -0,0 +1,25 @@
+#
+# $Id$
+#
+# IsaMakefile for CTT
+#
+
+OUT = $(ISABELLE_OUTPUT_DIR)
+
+FILES =	ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \
+	Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML
+
+EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML
+
+$(OUT)/CTT: $(OUT)/Pure $(FILES)
+	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure CTT
+	@chmod -w $@
+
+$(OUT)/Pure:
+	@cd ../Pure; $(ISATOOL) make
+
+test: ex/ROOT.ML $(OUT)/CTT $(EX_FILES)
+	@$(ISABELLE) -e 'make_html := $(ISABELLE_HTML); exit_use"ex/ROOT.ML"; quit();' \
+	  -rq $(OUT)/CTT
+
+.PRECIOUS: $(OUT)/Pure $(OUT)/CTT