29 Pure: |
29 Pure: |
30 @cd $(SRC)/Pure; $(ISATOOL) make Pure |
30 @cd $(SRC)/Pure; $(ISATOOL) make Pure |
31 |
31 |
32 $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \ |
32 $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \ |
33 $(SRC)/Provers/Arith/nat_transitive.ML $(SRC)/Provers/blast.ML \ |
33 $(SRC)/Provers/Arith/nat_transitive.ML $(SRC)/Provers/blast.ML \ |
34 $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML \ |
34 $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ |
35 $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \ |
35 $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \ |
36 $(SRC)/Pure/section_utils.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \ |
36 $(SRC)/Provers/splitter.ML $(SRC)/Pure/section_utils.ML \ |
37 $(SRC)/TFL/rules.new.sml $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml \ |
37 $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.new.sml \ |
38 $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig \ |
38 $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml $(SRC)/TFL/tfl.sig \ |
39 $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml \ |
39 $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \ |
40 $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig \ |
40 $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \ |
41 $(SRC)/TFL/utils.sml Arith.ML Arith.thy Divides.ML Divides.thy \ |
41 $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \ |
42 Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \ |
42 Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy \ |
43 Inductive.ML Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML \ |
43 Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.ML \ |
44 Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy \ |
44 Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \ |
45 Ord.ML Ord.thy Power.ML Power.thy Prod.ML Prod.thy ROOT.ML RelPow.ML \ |
45 Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \ |
46 RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \ |
46 Power.ML Power.thy Prod.ML Prod.thy ROOT.ML RelPow.ML RelPow.thy \ |
47 Sum.ML Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy \ |
47 Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy Sum.ML \ |
48 Vimage.ML Vimage.thy WF.ML WF.thy \ |
48 Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy \ |
49 WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML cladata.ML \ |
49 WF.ML WF.thy WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML \ |
50 datatype.ML equalities.ML equalities.thy hologic.ML ind_syntax.ML \ |
50 cladata.ML datatype.ML equalities.ML equalities.thy hologic.ML \ |
51 indrule.ML indrule.thy intr_elim.ML intr_elim.thy mono.ML mono.thy \ |
51 ind_syntax.ML indrule.ML indrule.thy intr_elim.ML intr_elim.thy \ |
52 record.ML simpdata.ML subset.ML subset.thy thy_data.ML thy_syntax.ML \ |
52 mono.ML mono.thy record.ML simpdata.ML subset.ML subset.thy \ |
53 typedef.ML |
53 thy_data.ML thy_syntax.ML typedef.ML |
54 @$(ISATOOL) usedir -b $(OUT)/Pure HOL |
54 @$(ISATOOL) usedir -b $(OUT)/Pure HOL |
55 |
55 |
56 |
56 |
57 ## HOL-Subst |
57 ## HOL-Subst |
58 |
58 |