src/HOL/IsaMakefile
changeset 19564 d3e2f532459a
parent 19499 1a082c1257d7
child 19640 40ec89317425
     1.1 --- a/src/HOL/IsaMakefile	Fri May 05 16:50:58 2006 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri May 05 17:17:21 2006 +0200
     1.3 @@ -120,7 +120,17 @@
     1.4    antisym_setup.ML arith_data.ML blastdata.ML cladata.ML			\
     1.5    document/root.tex hologic.ML simpdata.ML ResAtpMethods.thy 			\
     1.6    Tools/res_atp_provers.ML Tools/res_atp_methods.ML	\
     1.7 -  Tools/res_hol_clause.ML
     1.8 +  Tools/res_hol_clause.ML	\
     1.9 +  Tools/function_package/fundef_common.ML 	\
    1.10 +  Tools/function_package/fundef_lib.ML 	\
    1.11 +  Tools/function_package/context_tree.ML 	\
    1.12 +  Tools/function_package/fundef_prep.ML 	\
    1.13 +  Tools/function_package/fundef_proof.ML 	\
    1.14 +  Tools/function_package/termination.ML 	\
    1.15 +  Tools/function_package/fundef_package.ML 	\
    1.16 +  Tools/function_package/auto_term.ML 	\
    1.17 +  Tools/function_package/fundef_datatype.ML 	\
    1.18 +  FunDef.thy Accessible_Part.thy 
    1.19  	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
    1.20  
    1.21  
    1.22 @@ -184,7 +194,7 @@
    1.23  
    1.24  HOL-Library: HOL $(LOG)/HOL-Library.gz
    1.25  
    1.26 -$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
    1.27 +$(LOG)/HOL-Library.gz: $(OUT)/HOL \
    1.28    Library/SetsAndFunctions.thy Library/BigO.thy \
    1.29    Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
    1.30    Library/FuncSet.thy Library/Library.thy \
    1.31 @@ -480,7 +490,7 @@
    1.32  
    1.33  HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
    1.34  
    1.35 -$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Library/Accessible_Part.thy \
    1.36 +$(LOG)/HOL-Lambda.gz: $(OUT)/HOL \
    1.37    Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
    1.38    Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
    1.39    Lambda/ParRed.thy Lambda/StrongNorm.thy Lambda/Type.thy \
    1.40 @@ -740,7 +750,7 @@
    1.41  
    1.42  HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
    1.43  
    1.44 -$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal Library/Accessible_Part.thy	\
    1.45 +$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal 	\
    1.46    Nominal/Examples/ROOT.ML Nominal/Examples/CR.thy Nominal/Examples/Class.thy	\
    1.47    Nominal/Examples/Fsub.thy Nominal/Examples/Lambda_mu.thy			\
    1.48    Nominal/Examples/Iteration.thy Nominal/Examples/Lam_substs.thy		\