--- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy Wed Oct 28 00:08:32 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy Wed Oct 28 00:23:39 2009 +0100
@@ -1,6 +1,5 @@
-theory Multivariate_Analysis imports
- Convex_Euclidean_Space
- Determinants
+theory Multivariate_Analysis
+imports Convex_Euclidean_Space Determinants
begin
end
--- a/src/HOL/Multivariate_Analysis/ROOT.ML Wed Oct 28 00:08:32 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/ROOT.ML Wed Oct 28 00:23:39 2009 +0100
@@ -1,6 +1,1 @@
-(*
- no_document use_thy "ThisTheory";
- use_thy "ThatTheory";
-*)
-
use_thy "Multivariate_Analysis";