--- a/src/HOL/IsaMakefile Mon May 08 20:58:49 2000 +0200
+++ b/src/HOL/IsaMakefile Mon May 08 20:59:30 2000 +0200
@@ -31,40 +31,40 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
- $(SRC)/Provers/Arith/cancel_sums.ML \
- $(SRC)/Provers/Arith/assoc_fold.ML \
- $(SRC)/Provers/Arith/combine_numerals.ML \
- $(SRC)/Provers/Arith/cancel_numerals.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 \
- $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml \
- $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
- $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
- $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
- $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
- Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
- Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
- HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
- Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML Integ/IntArith.thy \
- Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
- Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy \
- Integ/NatSimprocs.ML Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \
- Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \
- Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.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 \
- SVC_Oracle.ML SVC_Oracle.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/numeral_syntax.ML Tools/primrec_package.ML \
- Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.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 blastdata.ML \
- cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \
+$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
+ $(SRC)/Provers/Arith/cancel_sums.ML \
+ $(SRC)/Provers/Arith/assoc_fold.ML \
+ $(SRC)/Provers/Arith/combine_numerals.ML \
+ $(SRC)/Provers/Arith/cancel_numerals.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 \
+ $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml \
+ $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
+ $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
+ $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
+ $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
+ Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
+ Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
+ HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
+ Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML Integ/IntArith.thy \
+ Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
+ Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy \
+ Integ/NatSimprocs.ML Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \
+ Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \
+ Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML \
+ Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
+ Relation.ML Relation.thy Set.ML Set.thy String.thy SVC_Oracle.ML \
+ SVC_Oracle.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/numeral_syntax.ML Tools/primrec_package.ML \
+ Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.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 blastdata.ML \
+ 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
@@ -133,11 +133,11 @@
Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
- Induct/Multiset0.ML Induct/Multiset0.thy \
- Induct/Multiset.ML Induct/Multiset.thy \
- Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy \
- Induct/ROOT.ML Induct/SList.ML Induct/SList.thy Induct/ABexp.ML \
- Induct/ABexp.thy Induct/Term.ML Induct/Term.thy
+ Induct/Multiset0.ML Induct/Multiset0.thy Induct/Multiset.ML \
+ Induct/Multiset.thy Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML \
+ Induct/PropLog.thy Induct/ROOT.ML Induct/Sexp.ML Induct/Sexp.thy \
+ Induct/SList.ML Induct/SList.thy Induct/ABexp.ML Induct/ABexp.thy \
+ Induct/Term.ML Induct/Term.thy
@$(ISATOOL) usedir $(OUT)/HOL Induct