src/HOL/IsaMakefile
changeset 15697 681bcb7f0389
parent 15684 5ec4d21889d6
child 15731 29ae73d8a84e
equal deleted inserted replaced
15696:1da4ce092c0b 15697:681bcb7f0389
   113   Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
   113   Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
   114   blastdata.ML cladata.ML \
   114   blastdata.ML cladata.ML \
   115  Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
   115  Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
   116  Tools/res_axioms.ML Tools/res_types_sorts.ML \
   116  Tools/res_axioms.ML Tools/res_types_sorts.ML \
   117  Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\
   117  Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\
   118  Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML Tools/ATP/recon_reconstruct_proof.ML \
   118  Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML \
   119  Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \
   119  Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \
   120  Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML   Tools/ATP/modUnix.ML  \
   120  Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML   Tools/ATP/modUnix.ML  \
   121  Tools/ATP/watcher.sig Tools/ATP/watcher.ML   Tools/res_atp.ML\
   121  Tools/ATP/watcher.sig Tools/ATP/watcher.ML   Tools/res_atp.ML\
   122   document/root.tex hologic.ML simpdata.ML thy_syntax.ML
   122   document/root.tex hologic.ML simpdata.ML thy_syntax.ML
   123 	@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
   123 	@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL