author wenzelm Tue Aug 17 17:33:47 1999 +0200 (1999-08-17) changeset 7231 830d7d520592 parent 7230 4ca0d7839ff1 child 7232 6e7b6b8490e0
tuned;
 src/HOL/IsaMakefile file | annotate | diff | revisions
```     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
```