src/HOL/Real/HahnBanach/Subspace.thy

--- 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"