src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy

 	by (simp add: linearform_add [of H] 
                       real_add_mult_distrib);
       also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; 
         by simp;
       also; have "h y1 + a1 * xi = h' x1";
-        by (rule h'_definite [RS sym]);
+        by (rule h'_definite [symmetric]);
       also; have "h y2 + a2 * xi = h' x2"; 
-        by (rule h'_definite [RS sym]);
+        by (rule h'_definite [symmetric]);
       finally; show ?thesis; .;
     qed;
  
     txt{* We further have to show that $h'$ is multiplicative, 
     i.~e.\ $h'\ap (c \mult x_1) = c \cdot h'\ap x_1$

       also; from vs y1'; have "... = c * h y1 + c * a1 * xi"; 
 	by (simp add: linearform_mult [of H]);
       also; from vs y1'; have "... = c * (h y1 + a1 * xi)"; 
 	by (simp add: real_add_mult_distrib2 real_mult_assoc);
       also; have "h y1 + a1 * xi = h' x1"; 
-        by (rule h'_definite [RS sym]);
+        by (rule h'_definite [symmetric]);
       finally; show ?thesis; .;
     qed;
   qed;
 qed;
 

       have "- a * (p (rinv a \<cdot> y + x0)) = p (a \<cdot> (rinv a \<cdot> y + x0))";
         by (simp add: seminorm_abs_homogenous abs_minus_eqI2);
       also; from nz vs y; have "... = p (y + a \<cdot> x0)";
         by (simp add: vs_add_mult_distrib1);
       also; from nz vs y; have "a * (h (rinv a \<cdot> y)) =  h y";
-        by (simp add: linearform_mult [RS sym]);
+        by (simp add: linearform_mult [symmetric]);
       finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
 
       hence "h y + a * xi <= h y + p (y + a \<cdot> x0) - h y";
         by (simp add: real_add_left_cancel_le);
       thus ?thesis; by simp;

       have "a * p (rinv a \<cdot> y + x0) = p (a \<cdot> (rinv a \<cdot> y + x0))";
         by (simp add: seminorm_abs_homogenous abs_eqI2);
       also; from nz vs y; have "... = p (y + a \<cdot> x0)";
         by (simp add: vs_add_mult_distrib1);
       also; from nz vs y; have "a * h (rinv a \<cdot> y) = h y";
-        by (simp add: linearform_mult [RS sym]); 
+        by (simp add: linearform_mult [symmetric]); 
       finally; have "a * xi <= p (y + a \<cdot> x0) - h y"; .;
  
       hence "h y + a * xi <= h y + (p (y + a \<cdot> x0) - h y)";
         by (simp add: real_add_left_cancel_le);
       thus ?thesis; by simp;