# HG changeset patch
# User huffman
# Date 1313525272 25200
# Node ID 7e3a026f014f9ffee882a05359ea1608179e2f8d
# Parent  5f974bead4365a583087acc052b4b03904f133e8
Multivariate_Analysis includes Determinants.thy, but doesn't import it by default

diff -r 5f974bead436 -r 7e3a026f014f src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
--- 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
diff -r 5f974bead436 -r 7e3a026f014f src/HOL/Multivariate_Analysis/ROOT.ML
--- 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"];