--- a/src/HOL/IsaMakefile Fri Feb 06 15:15:27 2009 +0100
+++ b/src/HOL/IsaMakefile Fri Feb 06 15:15:32 2009 +0100
@@ -15,6 +15,7 @@
HOL-Auth \
HOL-AxClasses \
HOL-Bali \
+ HOL-Decision_Procs \
HOL-Extraction \
HOL-HahnBanach \
HOL-Hoare \
@@ -36,7 +37,6 @@
HOL-Nominal-Examples \
HOL-NumberTheory \
HOL-Prolog \
- HOL-Reflection \
HOL-SET-Protocol \
HOL-SizeChange \
HOL-Statespace \
@@ -315,7 +315,7 @@
Library/Abstract_Rat.thy \
Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy \
Library/Executable_Set.thy Library/Infinite_Set.thy \
- Library/FuncSet.thy Library/Dense_Linear_Order.thy \
+ Library/FuncSet.thy \
Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy \
Library/Multiset.thy Library/Permutation.thy \
Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy \
@@ -658,6 +658,24 @@
@$(ISABELLE_TOOL) usedir $(OUT)/HOL SizeChange
+## HOL-Decision_Procs
+
+HOL-Decision_Procs: HOL $(LOG)/HOL-Decision_Procs.gz
+
+$(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \
+ Decision_Procs/Approximation.thy \
+ Decision_Procs/Cooper.thy \
+ Decision_Procs/cooper_tac.ML \
+ Decision_Procs/Dense_Linear_Order.thy \
+ Decision_Procs/Ferrack.thy \
+ Decision_Procs/ferrack_tac.ML \
+ Decision_Procs/MIR.thy \
+ Decision_Procs/mir_tac.ML \
+ Decision_Procs/Decision_Procs.thy \
+ Decision_Procs/ROOT.ML
+ @$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
+
+
## HOL-Lambda
HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
@@ -680,22 +698,6 @@
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
-## HOL-Reflection
-
-HOL-Reflection: HOL $(LOG)/HOL-Reflection.gz
-
-$(LOG)/HOL-Reflection.gz: $(OUT)/HOL \
- Reflection/Approximation.thy \
- Reflection/Cooper.thy \
- Reflection/cooper_tac.ML \
- Reflection/Ferrack.thy \
- Reflection/ferrack_tac.ML \
- Reflection/MIR.thy \
- Reflection/mir_tac.ML \
- Reflection/ROOT.ML
- @$(ISABELLE_TOOL) usedir $(OUT)/HOL Reflection
-
-
## HOL-W0
HOL-W0: HOL $(LOG)/HOL-W0.gz