--- a/src/HOL/IsaMakefile Tue Jul 06 21:06:51 1999 +0200
+++ b/src/HOL/IsaMakefile Tue Jul 06 21:08:30 1999 +0200
@@ -31,9 +31,9 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \
- $(SRC)/Provers/Arith/fast_lin_arith.ML \
- $(SRC)/Provers/Arith/abel_cancel.ML $(SRC)/Provers/blast.ML \
+$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
+ $(SRC)/Provers/Arith/cancel_sums.ML \
+ $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
$(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
@@ -49,18 +49,19 @@
Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \
Integ/Int.thy Integ/simproc.ML Lfp.ML Lfp.thy List.ML List.thy \
Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy \
- Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy Prod.ML \
- Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
+ Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy \
+ Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
Sum.ML Sum.thy Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \
Tools/datatype_package.ML Tools/datatype_prop.ML \
Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
- Tools/inductive_package.ML Tools/primrec_package.ML \
- Tools/recdef_package.ML Tools/record_package.ML \
- Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
- Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy cladata.ML \
- equalities.ML equalities.thy hologic.ML mono.ML mono.thy simpdata.ML \
- subset.ML subset.thy thy_syntax.ML
+ Tools/inductive_package.ML Tools/numeral_syntax.ML \
+ Tools/primrec_package.ML Tools/recdef_package.ML \
+ Tools/record_package.ML Tools/typedef_package.ML Trancl.ML \
+ Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
+ WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML equalities.thy \
+ hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \
+ thy_syntax.ML
@$(ISATOOL) usedir -b $(OUT)/Pure HOL