src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
 changeset 44170 510ac30f44c0 parent 44167 e81d676d598e child 44211 bd7c586b902e
```     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Aug 12 07:18:28 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Aug 12 09:17:24 2011 -0700
1.3 @@ -762,7 +762,7 @@
1.4  apply auto
1.5  apply (rule span_mul)
1.6  apply (rule span_superset)
1.7 -apply (auto simp add: Collect_def mem_def)
1.8 +apply auto
1.9  done
1.10
1.11  lemma finite_stdbasis: "finite {cart_basis i ::real^'n |i. i\<in> (UNIV:: 'n set)}" (is "finite ?S")
1.12 @@ -785,12 +785,12 @@
1.13  proof-
1.14    let ?U = "UNIV :: 'n set"
1.15    let ?B = "cart_basis ` S"
1.16 -  let ?P = "\<lambda>(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x\$i =0"
1.17 +  let ?P = "{(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x\$i =0}"
1.18   {fix x::"real^_" assume xS: "x\<in> ?B"
1.19 -   from xS have "?P x" by auto}
1.20 +   from xS have "x \<in> ?P" by auto}
1.21   moreover
1.22   have "subspace ?P"
1.23 -   by (auto simp add: subspace_def Collect_def mem_def)
1.24 +   by (auto simp add: subspace_def)
1.25   ultimately show ?thesis
1.26     using x span_induct[of ?B ?P x] iS by blast
1.27  qed
1.28 @@ -830,7 +830,7 @@
1.29      from equalityD2[OF span_stdbasis]
1.30      have IU: " (UNIV :: (real^'m) set) \<subseteq> span ?I" by blast
1.31      from linear_eq[OF lf lg IU] fg x
1.32 -    have "f x = g x" unfolding Collect_def  Ball_def mem_def by metis}
1.33 +    have "f x = g x" unfolding Ball_def mem_Collect_eq by metis}
1.34    then show ?thesis by (auto intro: ext)
1.35  qed
1.36
```