src/HOL/Real/HahnBanach/HahnBanach.thy

       proof -;
         have "EX H h. graph H h = g & is_linearform H h 
           & is_subspace H E & is_subspace F H
           & graph F f <= graph H h
           & (ALL x:H. h x <= p x)"; by (simp! add: norm_pres_extension_D);
-        thus ?thesis; by blast;
+        thus ?thesis; by (elim exE conjE) rule;
       qed;
       have h: "is_vectorspace H"; ..;
 
 txt {* We show that $h$ is defined on whole $E$ by classical contradiction.  *}; 
 

                 finally; have "h v - h u <= p (v + x0) + p (u + x0)"; .;
 
                 thus "- p (u + x0) - h u <= p (v + x0) - h v";
                   by (rule real_diff_ineq_swap);
               qed;
-              thus ?thesis; by blast;
+              thus ?thesis; by rule rule;
             qed;
 
 txt {* Define the extension $h_0$ of $h$ to $H_0$ using $\xi$.  *};
 
             def h0 == "\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0