# HG changeset patch
# User boehmes
# Date 1260540372 -3600
# Node ID a03f3f9874f611dbca80a68a06b3675c3b84a753
# Parent  53a8f294d60f246aa10437841f572ebfcdc32c74
depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)

diff -r 53a8f294d60f -r a03f3f9874f6 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