author  wenzelm 
Thu, 04 Oct 2001 15:27:13 +0200  
changeset 11676  d04e96f8b0fd 
parent 9888  c5622848bf18 
child 11771  b7b100a2de1d 
permissions  rwrr 
2433  1 
# 
2 
# $Id$ 

3 
# 

4 
# IsaMakefile for FOL 

5 
# 

6 

4518  7 
## targets 
8 

9 
default: FOL 

10 
images: FOL 

11 
test: FOLex 

12 
all: images test 

13 

14 

15 
## global settings 

16 

17 
SRC = $(ISABELLE_HOME)/src 

3118  18 
OUT = $(ISABELLE_OUTPUT) 
4447  19 
LOG = $(OUT)/log 
2433  20 

3233  21 

4518  22 
## FOL 
23 

24 
FOL: Pure $(OUT)/FOL 

2433  25 

4518  26 
Pure: 
27 
@cd $(SRC)/Pure; $(ISATOOL) make Pure 

2433  28 

9157  29 
$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML $(SRC)/Provers/make_elim.ML \ 
4685  30 
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ 
11676
d04e96f8b0fd
added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;
wenzelm
parents:
9888
diff
changeset

31 
$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \ 
d04e96f8b0fd
added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;
wenzelm
parents:
9888
diff
changeset

32 
$(SRC)/Provers/rulify.ML $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \ 
d04e96f8b0fd
added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;
wenzelm
parents:
9888
diff
changeset

33 
FOL.ML FOL.thy FOL_lemmas1.ML FOL_lemmas2.ML IFOL.ML IFOL.thy \ 
d04e96f8b0fd
added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;
wenzelm
parents:
9888
diff
changeset

34 
IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML document/root.tex \ 
d04e96f8b0fd
added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;
wenzelm
parents:
9888
diff
changeset

35 
fologic.ML hypsubstdata.ML intprover.ML simpdata.ML 
2821  36 
@$(ISATOOL) usedir b $(OUT)/Pure FOL 
2433  37 

4518  38 

39 
## FOLex 

40 

41 
FOLex: FOL $(LOG)/FOLex.gz 

2433  42 

4518  43 
$(LOG)/FOLex.gz: $(OUT)/FOL ex/If.ML ex/If.thy ex/IffOracle.ML \ 
44 
ex/IffOracle.thy ex/List.ML ex/List.thy ex/Nat.ML ex/Nat.thy \ 

11676
d04e96f8b0fd
added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;
wenzelm
parents:
9888
diff
changeset

45 
ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy ex/Prolog.ML \ 
d04e96f8b0fd
added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;
wenzelm
parents:
9888
diff
changeset

46 
ex/Prolog.thy ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML \ 
d04e96f8b0fd
added Provers/induct_method.ML, document/root.tex, ex/Natural_Numbers.thy;
wenzelm
parents:
9888
diff
changeset

47 
ex/int.thy ex/intro.ML ex/prop.ML ex/quant.ML 
2821  48 
@$(ISATOOL) usedir $(OUT)/FOL ex 
2433  49 

4518  50 

51 
## clean 

4447  52 

53 
clean: 

4518  54 
@rm f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOLex.gz 