Multivariate_Analysis includes Determinants.thy, but doesn't import it by default
authorhuffman
Tue, 16 Aug 2011 13:07:52 -0700
changeset 44229 7e3a026f014f
parent 44228 5f974bead436
child 44230 47e6986336f5
child 44233 aa74ce315bae
child 44243 d58864221eef
Multivariate_Analysis includes Determinants.thy, but doesn't import it by default
src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
src/HOL/Multivariate_Analysis/ROOT.ML
--- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Tue Aug 16 07:56:17 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Tue Aug 16 13:07:52 2011 -0700
@@ -1,5 +1,5 @@
 theory Multivariate_Analysis
-imports Fashoda Extended_Real_Limits Determinants
+imports Fashoda Extended_Real_Limits
 begin
 
 end
--- a/src/HOL/Multivariate_Analysis/ROOT.ML	Tue Aug 16 07:56:17 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/ROOT.ML	Tue Aug 16 13:07:52 2011 -0700
@@ -1,1 +1,1 @@
-use_thys ["Multivariate_Analysis"];
+use_thys ["Multivariate_Analysis", "Determinants"];