# HG changeset patch # User wenzelm # Date 934904027 -7200 # Node ID 830d7d52059292d6c657280561397ab2c052be7a # Parent 4ca0d7839ff1dfa8d40f2249669a1bea7b98504b tuned; diff -r 4ca0d7839ff1 -r 830d7d520592 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Aug 17 17:30:08 1999 +0200 +++ b/src/HOL/IsaMakefile Tue Aug 17 17:33:47 1999 +0200 @@ -32,9 +32,9 @@ @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_coeff.ML \ + $(SRC)/Provers/Arith/cancel_sums.ML \ + $(SRC)/Provers/Arith/assoc_fold.ML \ + $(SRC)/Provers/Arith/combine_coeff.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 \ @@ -48,26 +48,23 @@ Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \ Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \ Inductive.thy Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML \ - Integ/Equiv.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/simproc.ML \ - Lfp.ML Lfp.thy List.ML List.thy \ + Integ/Equiv.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/simproc.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 \ 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 cladata.ML equalities.ML equalities.thy \ - hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \ - thy_syntax.ML + 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 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