# HG changeset patch
# User wenzelm
# Date 852732233 -3600
# Node ID 88f15198950f1960bf06cdf90eaea2fa33ec5e6c
# Parent  82f105e8a0f93ef90f8f46085ed60ad690f3a1ab
IsaMakefile for Sequents;

diff -r 82f105e8a0f9 -r 88f15198950f src/Sequents/IsaMakefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/IsaMakefile	Wed Jan 08 15:03:53 1997 +0100
@@ -0,0 +1,30 @@
+#
+# $Id$
+#
+# IsaMakefile for Sequents
+#
+
+OUT = $(ISABELLE_OUTPUT_DIR)
+
+NAMES = ILL LK S4 S43 T
+FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)
+
+ILL_NAMES = ILL_predlog washing
+EX_FILES = ex/ROOT.ML \
+    ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML ex/LK/quant.ML \
+    ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML ex/Modal/Tthms.ML \
+    ex/ILL/ILL_kleene_lemmas.ML \
+    $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
+
+$(OUT)/Sequents: $(OUT)/Pure $(FILES)
+	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure Sequents
+	@chmod -w $@
+
+$(OUT)/Pure:
+	@cd ../Pure; $(ISATOOL) make
+
+test: $(OUT)/Sequents $(EX_FILES)
+	@$(ISABELLE) -e 'make_html := $(ISABELLE_HTML); exit_use"ex/ROOT.ML"; quit();' \
+	  -rq $(OUT)/Sequents
+
+.PRECIOUS: $(OUT)/Pure $(OUT)/Sequents