src/HOL/IsaMakefile
changeset 7142 89e0ff71d113
parent 7125 df7cf6e85501
child 7161 7845a5cafbc6
equal deleted inserted replaced
7141:a67dde8820c0 7142:89e0ff71d113
    54   Lfp.ML Lfp.thy List.ML List.thy \
    54   Lfp.ML Lfp.thy List.ML List.thy \
    55   Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy \
    55   Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy \
    56   Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy \
    56   Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy \
    57   Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
    57   Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
    58   Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
    58   Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
       
    59   SVC_Oracle.ML SVC_Oracle.thy \
    59   Sum.ML Sum.thy Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \
    60   Sum.ML Sum.thy Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \
    60   Tools/datatype_package.ML Tools/datatype_prop.ML \
    61   Tools/datatype_package.ML Tools/datatype_prop.ML \
    61   Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
    62   Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
    62   Tools/inductive_package.ML Tools/numeral_syntax.ML \
    63   Tools/inductive_package.ML Tools/numeral_syntax.ML \
    63   Tools/primrec_package.ML Tools/recdef_package.ML \
    64   Tools/primrec_package.ML Tools/recdef_package.ML \
    64   Tools/record_package.ML Tools/typedef_package.ML Trancl.ML \
    65   Tools/record_package.ML Tools/svc_funcs.ML \
       
    66   Tools/typedef_package.ML Trancl.ML \
    65   Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
    67   Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
    66   WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML equalities.thy \
    68   WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML equalities.thy \
    67   hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \
    69   hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \
    68   thy_syntax.ML
    70   thy_syntax.ML
    69 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    71 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL