author  nipkow 
Mon, 17 Dec 2001 14:27:18 +0100  
changeset 12526  1b9db2581fe2 
parent 12370  f9e6af324d35 
child 13301  c505fc950cbe 
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 \ 
12526
1b9db2581fe2
mods due to changed 1point simprocs (quantifier1).
nipkow
parents:
12370
diff
changeset

32 
$(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

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 

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

43 
$(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

44 
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

45 
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

46 
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

47 
ex/foundn.ML ex/int.ML 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 