author huffman Wed Aug 24 15:32:40 2011 -0700 (2011-08-24) changeset 44517 68e8eb0ce8aa parent 44516 d9a496ae5d9d child 44518 219a6fe4cfae
minimize imports
```     1.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 24 15:06:13 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 24 15:32:40 2011 -0700
1.3 @@ -8,8 +8,6 @@
1.4  imports
1.5    Euclidean_Space
1.6    "~~/src/HOL/Library/Infinite_Set"
1.7 -  L2_Norm
1.8 -  "~~/src/HOL/Library/Convex"
1.9  begin
1.10
1.11  lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
1.12 @@ -63,7 +61,7 @@
1.13  *)
1.14
1.15  lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
1.16 -  by (simp add: setL2_def power2_eq_square)
1.17 +  by (simp add: power2_eq_square)
1.18
1.19  lemma norm_cauchy_schwarz:
1.20    shows "inner x y <= norm x * norm y"
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 24 15:06:13 2011 -0700
2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 24 15:32:40 2011 -0700
2.3 @@ -7,7 +7,7 @@
2.4  header {* Elementary topology in Euclidean space. *}
2.5
2.6  theory Topology_Euclidean_Space
2.7 -imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
2.8 +imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm
2.9  begin
2.10
2.11  (* to be moved elsewhere *)
2.12 @@ -20,7 +20,7 @@
2.13    apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
2.14    apply(rule member_le_setL2) by auto
2.15
2.16 -subsection {* General notion of a topologies as values *}
2.17 +subsection {* General notion of a topology as a value *}
2.18
2.19  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))"
2.20  typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
```