changeset 9906 | 5c027cca6262 |
parent 9623 | 3ade112482af |
child 9941 | fe05af7ec816 |
--- a/src/HOL/Real/HahnBanach/Subspace.thy Thu Sep 07 21:06:55 2000 +0200 +++ b/src/HOL/Real/HahnBanach/Subspace.thy Thu Sep 07 21:10:11 2000 +0200 @@ -227,7 +227,7 @@ "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)" by (unfold vs_sum_def) fast -lemmas vs_sumE = vs_sumD [THEN iffD1, elimify, standard] +lemmas vs_sumE = vs_sumD [THEN iffD1, elimified, standard] lemma vs_sumI [intro?]: "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"