src/HOL/IsaMakefile
changeset 7699 09d8fd81cc1f
parent 7629 68e155f81f88
child 7760 43f8d28dbc6e
     1.1 --- a/src/HOL/IsaMakefile	Mon Oct 04 21:41:19 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Oct 04 21:43:05 1999 +0200
     1.3 @@ -41,31 +41,30 @@
     1.4    $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
     1.5    $(SRC)/Pure/section_utils.ML $(SRC)/TFL/dcterm.sml \
     1.6    $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml $(SRC)/TFL/rules.sig \
     1.7 -  $(SRC)/TFL/sys.sml $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
     1.8 -  $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
     1.9 -  $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
    1.10 -  $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
    1.11 -  Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
    1.12 -  Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
    1.13 -  HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
    1.14 -  Integ/Equiv.ML Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy \
    1.15 -  Integ/Int.ML Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy \
    1.16 -  Integ/NatBin.ML Integ/NatBin.thy Integ/simproc.ML Lfp.ML Lfp.thy \
    1.17 -  List.ML List.thy Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML \
    1.18 -  NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML \
    1.19 -  Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
    1.20 -  RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
    1.21 -  String.thy SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy \
    1.22 -  Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \
    1.23 -  Tools/datatype_package.ML Tools/datatype_prop.ML \
    1.24 -  Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
    1.25 -  Tools/inductive_package.ML Tools/numeral_syntax.ML \
    1.26 -  Tools/primrec_package.ML Tools/recdef_package.ML \
    1.27 -  Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
    1.28 -  Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML \
    1.29 -  WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML cladata.ML equalities.ML \
    1.30 -  equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
    1.31 -  subset.thy thy_syntax.ML
    1.32 +  $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig \
    1.33 +  $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml \
    1.34 +  $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig \
    1.35 +  $(SRC)/TFL/utils.sml Arith.ML Arith.thy Calculation.thy Datatype.thy \
    1.36 +  Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML \
    1.37 +  Gfp.thy HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML \
    1.38 +  Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML \
    1.39 +  Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \
    1.40 +  Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML \
    1.41 +  Integ/NatBin.thy Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \
    1.42 +  Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \
    1.43 +  Option.thy Ord.ML Ord.thy Power.ML Power.thy Prod.ML Prod.thy \
    1.44 +  ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy Relation.ML \
    1.45 +  Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
    1.46 +  SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
    1.47 +  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
    1.48 +  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
    1.49 +  Tools/induct_method.ML Tools/inductive_package.ML \
    1.50 +  Tools/numeral_syntax.ML Tools/primrec_package.ML \
    1.51 +  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
    1.52 +  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
    1.53 +  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML \
    1.54 +  cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \
    1.55 +  simpdata.ML subset.ML subset.thy thy_syntax.ML
    1.56  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    1.57  
    1.58