src/HOL/IsaMakefile
changeset 15774 9df37a0e935d
parent 15771 08cc20626a0f
child 15779 aed221aff642
equal deleted inserted replaced
15773:f14ae2432710 15774:9df37a0e935d
   112   Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
   112   Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
   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_order_clauses.ML\
   118  Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.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
   124 
   124 
   125 
   125