src/HOL/IsaMakefile
changeset 15684 5ec4d21889d6
parent 15678 28cc2314c7ff
child 15697 681bcb7f0389
     1.1 --- a/src/HOL/IsaMakefile	Fri Apr 08 10:50:02 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 08 18:43:39 2005 +0200
     1.3 @@ -100,25 +100,25 @@
     1.4    Orderings.ML Orderings.thy Ring_and_Field.thy\
     1.5    Set.ML Set.thy SetInterval.thy \
     1.6    Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
     1.7 -  Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
     1.8 -  Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \
     1.9 -  Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \
    1.10 -  Tools/meson.ML Tools/numeral_syntax.ML \
    1.11 -  Tools/primrec_package.ML Tools/prop_logic.ML \
    1.12 -  Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
    1.13 -  Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
    1.14 -  Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
    1.15 -  Tools/split_rule.ML Tools/typedef_package.ML \
    1.16 + Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
    1.17 + Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \
    1.18 + Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \
    1.19 + Tools/meson.ML Tools/numeral_syntax.ML \
    1.20 + Tools/primrec_package.ML Tools/prop_logic.ML \
    1.21 + Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
    1.22 + Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
    1.23 + Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
    1.24 + Tools/split_rule.ML Tools/typedef_package.ML \
    1.25    Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
    1.26    Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
    1.27    blastdata.ML cladata.ML \
    1.28 -  Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
    1.29 -  Tools/res_axioms.ML Tools/res_types_sorts.ML \
    1.30 -  Tools/ATP/recon_prelim.ML  Tools/ATP/recon_gandalf_base.ML  Tools/ATP/recon_order_clauses.ML\
    1.31 -  Tools/ATP/recon_translate_proof.ML   Tools/ATP/recon_parse.ML   Tools/ATP/recon_reconstruct_proof.ML \
    1.32 -  Tools/ATP/recon_transfer_proof.ML  Tools/ATP/myres_axioms.ML   Tools/ATP/res_clasimpset.ML \
    1.33 -  Tools/ATP/VampireCommunication.ML  Tools/ATP/SpassCommunication.ML     Tools/ATP/modUnix.ML  \
    1.34 -  Tools/ATP/watcher.sig  Tools/ATP/watcher.ML    Tools/res_atp.ML\
    1.35 + Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
    1.36 + Tools/res_axioms.ML Tools/res_types_sorts.ML \
    1.37 + Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\
    1.38 + Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML Tools/ATP/recon_reconstruct_proof.ML \
    1.39 + Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \
    1.40 + Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML   Tools/ATP/modUnix.ML  \
    1.41 + Tools/ATP/watcher.sig Tools/ATP/watcher.ML   Tools/res_atp.ML\
    1.42    document/root.tex hologic.ML simpdata.ML thy_syntax.ML
    1.43  	@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
    1.44