29 HOL: Pure $(OUT)/HOL |
29 HOL: Pure $(OUT)/HOL |
30 |
30 |
31 Pure: |
31 Pure: |
32 @cd $(SRC)/Pure; $(ISATOOL) make Pure |
32 @cd $(SRC)/Pure; $(ISATOOL) make Pure |
33 |
33 |
34 $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \ |
34 $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \ |
35 $(SRC)/Provers/Arith/fast_lin_arith.ML \ |
35 $(SRC)/Provers/Arith/cancel_sums.ML \ |
36 $(SRC)/Provers/Arith/abel_cancel.ML $(SRC)/Provers/blast.ML \ |
36 $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \ |
37 $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ |
37 $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ |
38 $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \ |
38 $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \ |
39 $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \ |
39 $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \ |
40 $(SRC)/Pure/section_utils.ML $(SRC)/TFL/dcterm.sml \ |
40 $(SRC)/Pure/section_utils.ML $(SRC)/TFL/dcterm.sml \ |
41 $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml $(SRC)/TFL/rules.sig \ |
41 $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml $(SRC)/TFL/rules.sig \ |
47 Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \ |
47 Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \ |
48 Inductive.thy Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML \ |
48 Inductive.thy Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML \ |
49 Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \ |
49 Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \ |
50 Integ/Int.thy Integ/simproc.ML Lfp.ML Lfp.thy List.ML List.thy \ |
50 Integ/Int.thy Integ/simproc.ML Lfp.ML Lfp.thy List.ML List.thy \ |
51 Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy \ |
51 Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy \ |
52 Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy Prod.ML \ |
52 Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy \ |
53 Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \ |
53 Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \ |
54 Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \ |
54 Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \ |
55 Sum.ML Sum.thy Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \ |
55 Sum.ML Sum.thy Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \ |
56 Tools/datatype_package.ML Tools/datatype_prop.ML \ |
56 Tools/datatype_package.ML Tools/datatype_prop.ML \ |
57 Tools/datatype_rep_proofs.ML Tools/induct_method.ML \ |
57 Tools/datatype_rep_proofs.ML Tools/induct_method.ML \ |
58 Tools/inductive_package.ML Tools/primrec_package.ML \ |
58 Tools/inductive_package.ML Tools/numeral_syntax.ML \ |
59 Tools/recdef_package.ML Tools/record_package.ML \ |
59 Tools/primrec_package.ML Tools/recdef_package.ML \ |
60 Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \ |
60 Tools/record_package.ML Tools/typedef_package.ML Trancl.ML \ |
61 Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy cladata.ML \ |
61 Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \ |
62 equalities.ML equalities.thy hologic.ML mono.ML mono.thy simpdata.ML \ |
62 WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML equalities.thy \ |
63 subset.ML subset.thy thy_syntax.ML |
63 hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \ |
|
64 thy_syntax.ML |
64 @$(ISATOOL) usedir -b $(OUT)/Pure HOL |
65 @$(ISATOOL) usedir -b $(OUT)/Pure HOL |
65 |
66 |
66 |
67 |
67 ## HOL-Subst |
68 ## HOL-Subst |
68 |
69 |