src/FOLP/IsaMakefile
changeset 26322 eaf634e975fa
parent 25991 31b38a39e589
child 26408 6964c4799f47
--- a/src/FOLP/IsaMakefile	Tue Mar 18 21:57:36 2008 +0100
+++ b/src/FOLP/IsaMakefile	Tue Mar 18 22:19:18 2008 +0100
@@ -26,7 +26,7 @@
 Pure:
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
-$(OUT)/FOLP: $(OUT)/Pure FOLP_lemmas.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \
+$(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML \
   classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
 
@@ -35,8 +35,9 @@
 
 FOLP-ex: FOLP $(LOG)/FOLP-ex.gz
 
-$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/cla.ML ex/Foundation.thy \
-  ex/If.thy ex/int.ML ex/Intro.thy ex/Nat.thy \
+$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy \
+  ex/If.thy ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy   \
+  ex/Classical.thy					    \
   ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML
 	@$(ISATOOL) usedir $(OUT)/FOLP ex