src/HOL/IsaMakefile
changeset 17517 9dc9d3005ed2
parent 17507 507e519a0dad
child 17518 87b49367ee9b
equal deleted inserted replaced
17516:45164074dad4 17517:9dc9d3005ed2
    95   Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML		\
    95   Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML		\
    96   Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML		\
    96   Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML		\
    97   Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML			\
    97   Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML			\
    98   Tools/ATP/recon_transfer_proof.ML			\
    98   Tools/ATP/recon_transfer_proof.ML			\
    99   Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML		\
    99   Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML		\
   100   Tools/ATP/watcher.ML 	Tools/comm_ring.ML					\
   100   Tools/ATP/watcher.ML 					\
   101   Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML				\
   101   Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML				\
   102   Tools/datatype_codegen.ML Tools/datatype_package.ML				\
   102   Tools/datatype_codegen.ML Tools/datatype_package.ML				\
   103   Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
   103   Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
   104   Tools/datatype_rep_proofs.ML Tools/inductive_codegen.ML			\
   104   Tools/datatype_rep_proofs.ML Tools/inductive_codegen.ML			\
   105   Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
   105   Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
   186   Library/README.html Library/Continuity.thy \
   186   Library/README.html Library/Continuity.thy \
   187   Library/Nested_Environment.thy Library/Zorn.thy\
   187   Library/Nested_Environment.thy Library/Zorn.thy\
   188   Library/Library/ROOT.ML Library/Library/document/root.tex \
   188   Library/Library/ROOT.ML Library/Library/document/root.tex \
   189   Library/Library/document/root.bib Library/While_Combinator.thy \
   189   Library/Library/document/root.bib Library/While_Combinator.thy \
   190   Library/Product_ord.thy Library/Char_ord.thy \
   190   Library/Product_ord.thy Library/Char_ord.thy \
   191   Library/List_lexord.thy
   191   Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML
   192 	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
   192 	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
   193 
   193 
   194 
   194 
   195 ## HOL-Subst
   195 ## HOL-Subst
   196 
   196