depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)
authorboehmes
Fri, 11 Dec 2009 15:06:12 +0100
changeset 34067 a03f3f9874f6
parent 34053 53a8f294d60f
child 34068 a78307d72e58
depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)
src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Dec 10 22:28:55 2009 +0100
+++ b/src/HOL/IsaMakefile	Fri Dec 11 15:06:12 2009 +0100
@@ -1049,9 +1049,9 @@
 
 ## HOL-Multivariate_Analysis
 
-HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis
+HOL-Multivariate_Analysis: HOL-SMT $(OUT)/HOL-Multivariate_Analysis
 
-$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL		\
+$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL-SMT	\
   Multivariate_Analysis/ROOT.ML				\
   Multivariate_Analysis/Multivariate_Analysis.thy	\
   Multivariate_Analysis/Determinants.thy		\
@@ -1061,7 +1061,7 @@
   Multivariate_Analysis/Convex_Euclidean_Space.thy      \
   Multivariate_Analysis/Brouwer_Fixpoint.thy            \
   Multivariate_Analysis/Derivative.thy
-	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
+	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Multivariate_Analysis
 
 
 ## HOL-Probability