changeset 44887 | 7ca82df6e951 |
parent 32960 | 69916a850301 |
child 45605 | a89b4bc311a5 |
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Sun Sep 11 21:35:35 2011 +0200 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Sun Sep 11 22:55:26 2011 +0200 @@ -334,7 +334,7 @@ proof fix x assume "x \<in> H" with M cM graph - obtain H' h' where x: "x \<in> H'" and H'E: "H' \<unlhd> E" + obtain H' where x: "x \<in> H'" and H'E: "H' \<unlhd> E" by (rule some_H'h' [elim_format]) blast from H'E have "H' \<subseteq> E" .. with x show "x \<in> E" ..