author  wenzelm 
Sat, 09 Jul 2011 21:53:27 +0200  
changeset 43721  fad8634cee62 
parent 42799  4e33894aec6d 
child 44121  44adaa6db327 
permissions  rwrr 
2433  1 
# 
2 
# IsaMakefile for FOL 

3 
# 

4 

4518  5 
## targets 
6 

7 
default: FOL 

8 
images: FOL 

9 
test: FOLex 

10 
all: images test 

42138
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj  allows the use of "isabelle makeall smlnj";
krauss
parents:
41827
diff
changeset

11 
smlnj: all 
4518  12 

13 

14 
## global settings 

15 

16 
SRC = $(ISABELLE_HOME)/src 

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

3233  20 

4518  21 
## FOL 
22 

27203  23 
FOL: Pure $(OUT)/FOL 
2433  24 

4518  25 
Pure: 
28500  26 
@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure 
2433  27 

27203  28 
$(OUT)/Pure: Pure 
13301  29 

27203  30 
$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \ 
16019  31 
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ 
42793  32 
$(SRC)/Tools/case_product.ML $(SRC)/Tools/IsaPlanner/zipper.ML \ 
33 
$(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_tools.ML \ 

30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
29752
diff
changeset

34 
$(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \ 
27203  35 
$(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \ 
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset

36 
$(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \ 
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset

37 
$(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \ 
42793  38 
$(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML \ 
42799  39 
document/root.tex fologic.ML intprover.ML simpdata.ML 
28500  40 
@$(ISABELLE_TOOL) usedir p 2 b $(OUT)/Pure FOL 
2433  41 

4518  42 

43 
## FOLex 

44 

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

2433  46 

27203  47 
$(LOG)/FOLex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy \ 
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isarref;
wenzelm
parents:
37134
diff
changeset

48 
ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \ 
37134  49 
ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy \ 
50 
ex/Locale_Test/Locale_Test2.thy ex/Locale_Test/Locale_Test3.thy \ 

40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isarref;
wenzelm
parents:
37134
diff
changeset

51 
ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy \ 
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isarref;
wenzelm
parents:
37134
diff
changeset

52 
ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy \ 
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isarref;
wenzelm
parents:
37134
diff
changeset

53 
ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy \ 
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isarref;
wenzelm
parents:
37134
diff
changeset

54 
ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy 
28500  55 
@$(ISABELLE_TOOL) usedir $(OUT)/FOL ex 
2433  56 

4518  57 

58 
## clean 

4447  59 

60 
clean: 

27203  61 
@rm f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOLex.gz 