src/HOL/IsaMakefile
changeset 29823 0ab754d13ccd
parent 29813 3ccd86c214bf
child 29836 3d935e8b0bf7
     1.1 --- a/src/HOL/IsaMakefile	Fri Feb 06 15:15:27 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Feb 06 15:15:32 2009 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4    HOL-Auth \
     1.5    HOL-AxClasses \
     1.6    HOL-Bali \
     1.7 +  HOL-Decision_Procs \
     1.8    HOL-Extraction \
     1.9    HOL-HahnBanach \
    1.10    HOL-Hoare \
    1.11 @@ -36,7 +37,6 @@
    1.12    HOL-Nominal-Examples \
    1.13    HOL-NumberTheory \
    1.14    HOL-Prolog \
    1.15 -  HOL-Reflection \
    1.16    HOL-SET-Protocol \
    1.17    HOL-SizeChange \
    1.18    HOL-Statespace \
    1.19 @@ -315,7 +315,7 @@
    1.20    Library/Abstract_Rat.thy \
    1.21    Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy	\
    1.22    Library/Executable_Set.thy Library/Infinite_Set.thy			\
    1.23 -  Library/FuncSet.thy Library/Dense_Linear_Order.thy 	\
    1.24 +  Library/FuncSet.thy	\
    1.25    Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy	\
    1.26    Library/Multiset.thy Library/Permutation.thy	\
    1.27    Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy	\
    1.28 @@ -658,6 +658,24 @@
    1.29  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL SizeChange
    1.30  
    1.31  
    1.32 +## HOL-Decision_Procs
    1.33 +
    1.34 +HOL-Decision_Procs: HOL $(LOG)/HOL-Decision_Procs.gz
    1.35 +
    1.36 +$(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \
    1.37 +  Decision_Procs/Approximation.thy \
    1.38 +  Decision_Procs/Cooper.thy \
    1.39 +  Decision_Procs/cooper_tac.ML \
    1.40 +  Decision_Procs/Dense_Linear_Order.thy \
    1.41 +  Decision_Procs/Ferrack.thy \
    1.42 +  Decision_Procs/ferrack_tac.ML \
    1.43 +  Decision_Procs/MIR.thy \
    1.44 +  Decision_Procs/mir_tac.ML \
    1.45 +  Decision_Procs/Decision_Procs.thy \
    1.46 +  Decision_Procs/ROOT.ML
    1.47 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
    1.48 +
    1.49 +
    1.50  ## HOL-Lambda
    1.51  
    1.52  HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
    1.53 @@ -680,22 +698,6 @@
    1.54  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
    1.55  
    1.56  
    1.57 -## HOL-Reflection
    1.58 -
    1.59 -HOL-Reflection: HOL $(LOG)/HOL-Reflection.gz
    1.60 -
    1.61 -$(LOG)/HOL-Reflection.gz: $(OUT)/HOL \
    1.62 -  Reflection/Approximation.thy \
    1.63 -  Reflection/Cooper.thy \
    1.64 -  Reflection/cooper_tac.ML \
    1.65 -  Reflection/Ferrack.thy \
    1.66 -  Reflection/ferrack_tac.ML \
    1.67 -  Reflection/MIR.thy \
    1.68 -  Reflection/mir_tac.ML \
    1.69 -  Reflection/ROOT.ML
    1.70 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Reflection
    1.71 -
    1.72 -
    1.73  ## HOL-W0
    1.74  
    1.75  HOL-W0: HOL $(LOG)/HOL-W0.gz