# HG changeset patch
# User huffman
# Date 1396056080 25200
# Node ID 3bc95e0fa65192c26bd7531bde551fe726d6c083
# Parent  4e589bcab2570256a55ba801fc4641ee1f61d792
minimized imports

diff -r 4e589bcab257 -r 3bc95e0fa651 src/HOL/Multivariate_Analysis/Operator_Norm.thy
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Sat Mar 29 12:05:24 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Fri Mar 28 18:21:20 2014 -0700
@@ -6,7 +6,7 @@
 header {* Operator Norm *}
 
 theory Operator_Norm
-imports Linear_Algebra
+imports Complex_Main
 begin
 
 text {* This formulation yields zero if @{text 'a} is the trivial vector space. *}