# HG changeset patch
# User huffman
# Date 1314225160 25200
# Node ID 68e8eb0ce8aa6466667ae6b415364afcfe86cdae
# Parent  d9a496ae5d9db2c78e166c0a586ce63f15ddaa00
minimize imports

diff -r d9a496ae5d9d -r 68e8eb0ce8aa src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 24 15:06:13 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 24 15:32:40 2011 -0700
@@ -8,8 +8,6 @@
 imports
   Euclidean_Space
   "~~/src/HOL/Library/Infinite_Set"
-  L2_Norm
-  "~~/src/HOL/Library/Convex"
 begin
 
 lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
@@ -63,7 +61,7 @@
 *)
 
 lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
-  by (simp add: setL2_def power2_eq_square)
+  by (simp add: power2_eq_square)
 
 lemma norm_cauchy_schwarz:
   shows "inner x y <= norm x * norm y"
diff -r d9a496ae5d9d -r 68e8eb0ce8aa src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 24 15:06:13 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 24 15:32:40 2011 -0700
@@ -7,7 +7,7 @@
 header {* Elementary topology in Euclidean space. *}
 
 theory Topology_Euclidean_Space
-imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
+imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm
 begin
 
 (* to be moved elsewhere *)
@@ -20,7 +20,7 @@
   apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
   apply(rule member_le_setL2) by auto
 
-subsection {* General notion of a topologies as values *}
+subsection {* General notion of a topology as a value *}
 
 definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
 typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"