author  kleing 
Fri, 05 Jul 2002 11:18:05 +0200  
changeset 13301  c505fc950cbe 
parent 12526  1b9db2581fe2 
child 13550  5a176b8dda84 
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 

13301  29 
$(OUT)/Pure: Pure 
30 

9157  31 
$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML $(SRC)/Provers/make_elim.ML \ 
4685  32 
$(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

33 
$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \ 
12526
1b9db2581fe2
mods due to changed 1point simprocs (quantifier1).
nipkow
parents:
12370
diff
changeset

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

35 
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

36 
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

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

4518  40 

41 
## FOLex 

42 

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

2433  44 

12370
f9e6af324d35
added ex/First_Order_Logic.thy, ex/document/root.tex;
wenzelm
parents:
11771
diff
changeset

45 
$(LOG)/FOLex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.ML \ 
f9e6af324d35
added ex/First_Order_Logic.thy, ex/document/root.tex;
wenzelm
parents:
11771
diff
changeset

46 
ex/If.thy ex/IffOracle.ML ex/IffOracle.thy ex/List.ML ex/List.thy \ 
f9e6af324d35
added ex/First_Order_Logic.thy, ex/document/root.tex;
wenzelm
parents:
11771
diff
changeset

47 
ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy \ 
f9e6af324d35
added ex/First_Order_Logic.thy, ex/document/root.tex;
wenzelm
parents:
11771
diff
changeset

48 
ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/cla.ML ex/document/root.tex \ 
f9e6af324d35
added ex/First_Order_Logic.thy, ex/document/root.tex;
wenzelm
parents:
11771
diff
changeset

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

4518  52 

53 
## clean 

4447  54 

55 
clean: 

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