src/HOL/Real/HahnBanach/Subspace.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 9969 4753185f1dd2
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -227,7 +227,7 @@
     1.4    "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
     1.5      by (unfold vs_sum_def) fast
     1.6  
     1.7 -lemmas vs_sumE = vs_sumD [THEN iffD1, elimified, standard]
     1.8 +lemmas vs_sumE = vs_sumD [THEN iffD1, elim_format, standard]
     1.9  
    1.10  lemma vs_sumI [intro?]: 
    1.11    "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"