src/HOL/IsaMakefile
changeset 4707 abe6f28a38c1
parent 4657 941c9b169dc4
child 4729 e1888c0d3b36
     1.1 --- a/src/HOL/IsaMakefile	Mon Mar 09 16:14:32 1998 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Mar 09 16:14:46 1998 +0100
     1.3 @@ -31,26 +31,26 @@
     1.4  
     1.5  $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \
     1.6    $(SRC)/Provers/Arith/nat_transitive.ML $(SRC)/Provers/blast.ML \
     1.7 -  $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML \
     1.8 -  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
     1.9 -  $(SRC)/Pure/section_utils.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \
    1.10 -  $(SRC)/TFL/rules.new.sml $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml \
    1.11 -  $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig \
    1.12 -  $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml \
    1.13 -  $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig \
    1.14 -  $(SRC)/TFL/utils.sml Arith.ML Arith.thy Divides.ML Divides.thy \
    1.15 -  Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
    1.16 -  Inductive.ML Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML \
    1.17 -  Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy \
    1.18 -  Ord.ML Ord.thy Power.ML Power.thy Prod.ML Prod.thy ROOT.ML RelPow.ML \
    1.19 -  RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
    1.20 -  Sum.ML Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy \
    1.21 -  Vimage.ML Vimage.thy WF.ML WF.thy \
    1.22 -  WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML cladata.ML \
    1.23 -  datatype.ML equalities.ML equalities.thy hologic.ML ind_syntax.ML \
    1.24 -  indrule.ML indrule.thy intr_elim.ML intr_elim.thy mono.ML mono.thy \
    1.25 -  record.ML simpdata.ML subset.ML subset.thy thy_data.ML thy_syntax.ML \
    1.26 -  typedef.ML
    1.27 +  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    1.28 +  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
    1.29 +  $(SRC)/Provers/splitter.ML $(SRC)/Pure/section_utils.ML \
    1.30 +  $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.new.sml \
    1.31 +  $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml $(SRC)/TFL/tfl.sig \
    1.32 +  $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \
    1.33 +  $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \
    1.34 +  $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \
    1.35 +  Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy \
    1.36 +  Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.ML \
    1.37 +  Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \
    1.38 +  Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
    1.39 +  Power.ML Power.thy Prod.ML Prod.thy ROOT.ML RelPow.ML RelPow.thy \
    1.40 +  Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy Sum.ML \
    1.41 +  Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy \
    1.42 +  WF.ML WF.thy WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML \
    1.43 +  cladata.ML datatype.ML equalities.ML equalities.thy hologic.ML \
    1.44 +  ind_syntax.ML indrule.ML indrule.thy intr_elim.ML intr_elim.thy \
    1.45 +  mono.ML mono.thy record.ML simpdata.ML subset.ML subset.thy \
    1.46 +  thy_data.ML thy_syntax.ML typedef.ML
    1.47  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    1.48  
    1.49