src/FOLP/IsaMakefile
changeset 26408 6964c4799f47
parent 26322 eaf634e975fa
child 28500 4b79e5d3d0aa
     1.1 --- a/src/FOLP/IsaMakefile	Wed Mar 26 22:38:17 2008 +0100
     1.2 +++ b/src/FOLP/IsaMakefile	Wed Mar 26 22:38:55 2008 +0100
     1.3 @@ -26,8 +26,8 @@
     1.4  Pure:
     1.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     1.6  
     1.7 -$(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML \
     1.8 -  classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML
     1.9 +$(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML classical.ML	\
    1.10 +  hypsubst.ML intprover.ML simp.ML simpdata.ML
    1.11  	@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
    1.12  
    1.13  
    1.14 @@ -35,10 +35,11 @@
    1.15  
    1.16  FOLP-ex: FOLP $(LOG)/FOLP-ex.gz
    1.17  
    1.18 -$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy \
    1.19 -  ex/If.thy ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy   \
    1.20 -  ex/Classical.thy					    \
    1.21 -  ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML
    1.22 +$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy ex/If.thy	\
    1.23 +  ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy ex/Classical.thy	\
    1.24 +  ex/Prolog.ML ex/Prolog.thy ex/Propositional_Int.thy			\
    1.25 +  ex/Propositional_Cla.thy ex/Quantifiers_Int.thy			\
    1.26 +  ex/Quantifiers_Cla.thy
    1.27  	@$(ISATOOL) usedir $(OUT)/FOLP ex
    1.28  
    1.29