Multivariate_Analysis includes Determinants.thy, but doesn't import it by default
authorhuffman
Tue Aug 16 13:07:52 2011 -0700 (2011-08-16)
changeset 442297e3a026f014f
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
     1.1 --- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Tue Aug 16 07:56:17 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Tue Aug 16 13:07:52 2011 -0700
     1.3 @@ -1,5 +1,5 @@
     1.4  theory Multivariate_Analysis
     1.5 -imports Fashoda Extended_Real_Limits Determinants
     1.6 +imports Fashoda Extended_Real_Limits
     1.7  begin
     1.8  
     1.9  end
     2.1 --- a/src/HOL/Multivariate_Analysis/ROOT.ML	Tue Aug 16 07:56:17 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/ROOT.ML	Tue Aug 16 13:07:52 2011 -0700
     2.3 @@ -1,1 +1,1 @@
     2.4 -use_thys ["Multivariate_Analysis"];
     2.5 +use_thys ["Multivariate_Analysis", "Determinants"];