# 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"];