tuned;
authorwenzelm
Tue Aug 17 17:33:47 1999 +0200 (1999-08-17)
changeset 7231830d7d520592
parent 7230 4ca0d7839ff1
child 7232 6e7b6b8490e0
tuned;
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Tue Aug 17 17:30:08 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Aug 17 17:33:47 1999 +0200
     1.3 @@ -32,9 +32,9 @@
     1.4  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     1.5  
     1.6  $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
     1.7 -  $(SRC)/Provers/Arith/cancel_sums.ML		\
     1.8 -  $(SRC)/Provers/Arith/assoc_fold.ML		\
     1.9 -  $(SRC)/Provers/Arith/combine_coeff.ML		\
    1.10 +  $(SRC)/Provers/Arith/cancel_sums.ML \
    1.11 +  $(SRC)/Provers/Arith/assoc_fold.ML \
    1.12 +  $(SRC)/Provers/Arith/combine_coeff.ML \
    1.13    $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
    1.14    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    1.15    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
    1.16 @@ -48,26 +48,23 @@
    1.17    Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
    1.18    Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
    1.19    Inductive.thy Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML \
    1.20 -  Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy \
    1.21 -  Integ/Int.ML Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy \
    1.22 -  Integ/NatBin.ML Integ/NatBin.thy Integ/simproc.ML \
    1.23 -  Lfp.ML Lfp.thy List.ML List.thy \
    1.24 +  Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \
    1.25 +  Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML \
    1.26 +  Integ/NatBin.thy Integ/simproc.ML Lfp.ML Lfp.thy List.ML List.thy \
    1.27    Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy \
    1.28    Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy \
    1.29    Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
    1.30    Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
    1.31 -  SVC_Oracle.ML SVC_Oracle.thy \
    1.32 -  Sum.ML Sum.thy Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \
    1.33 -  Tools/datatype_package.ML Tools/datatype_prop.ML \
    1.34 -  Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
    1.35 -  Tools/inductive_package.ML Tools/numeral_syntax.ML \
    1.36 -  Tools/primrec_package.ML Tools/recdef_package.ML \
    1.37 -  Tools/record_package.ML Tools/svc_funcs.ML \
    1.38 -  Tools/typedef_package.ML Trancl.ML \
    1.39 -  Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
    1.40 -  WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML equalities.thy \
    1.41 -  hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \
    1.42 -  thy_syntax.ML
    1.43 +  SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
    1.44 +  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
    1.45 +  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
    1.46 +  Tools/induct_method.ML Tools/inductive_package.ML \
    1.47 +  Tools/numeral_syntax.ML Tools/primrec_package.ML \
    1.48 +  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
    1.49 +  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
    1.50 +  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy cladata.ML \
    1.51 +  equalities.ML equalities.thy hologic.ML mono.ML mono.thy simpdata.ML \
    1.52 +  subset.ML subset.thy thy_syntax.ML
    1.53  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    1.54  
    1.55