src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44286 8766839efb1b
parent 44282 f0de18b62d63
child 44342 8321948340ea
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 23:43:22 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 17:32:02 2011 -0700
     1.3 @@ -5570,9 +5570,6 @@
     1.4  
     1.5  subsection {* Some properties of a canonical subspace *}
     1.6  
     1.7 -(** move **)
     1.8 -declare euclidean_component_zero[simp]
     1.9 -
    1.10  lemma subspace_substandard:
    1.11    "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
    1.12    unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *)