src/HOL/Real/HahnBanach/FunctionNorm.thy

         from a; have le: "rabs (f x) <= c * norm x"; ..;
         have "y = rabs (f x) * rinv (norm x)";.;
         also; from _  le; have "... <= c * norm x * rinv (norm x)";
         proof (rule real_mult_le_le_mono2);
           show "0r <= rinv (norm x)";
-          proof (rule less_imp_le);
+          proof (rule real_less_imp_le);
             show "0r < rinv (norm x)";
             proof (rule real_rinv_gt_zero);
               show "0r < norm x"; ..;
             qed;
           qed;
-     (*** or:  by (rule less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero); ***)
+     (*** or:  by (rule real_less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero); ***)
         qed;
         also; have "... = c * (norm x * rinv (norm x))"; by (rule real_mult_assoc);
         also; have "(norm x * rinv (norm x)) = 1r"; 
         proof (rule real_mult_inv_right);
           show "norm x ~= 0r"; 

         "r = rabs (f x) * rinv (norm x)"; 
       show  "0r <= r";
       proof (simp!, rule real_le_mult_order);
         show "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero);
         show "0r <= rinv (norm x)";
-        proof (rule less_imp_le);
+        proof (rule real_less_imp_le);
           show "0r < rinv (norm x)"; 
           proof (rule real_rinv_gt_zero);
             show "0r < norm x"; ..;
           qed;
         qed;

 proof -; 
   assume "is_normed_vectorspace V norm" "x:V" and c: "is_continous V norm f";
   have v: "is_vectorspace V"; ..;
   assume "x:V";
   show "?thesis";
-  proof (rule case [of "x = <0>"]);
+  proof (rule case_split [of "x = <0>"]);
     assume "x ~= <0>";
     show "?thesis";
     proof -;
       have n: "0r <= norm x"; ..;
       have le: "rabs (f x) * rinv (norm x) <= function_norm V norm f"; 

   assume "is_normed_vectorspace V norm"; 
   assume c: "is_continous V norm f";
   assume fb: "ALL x:V. rabs (f x) <= c * norm x"
          and "0r <= c";
   show "Sup UNIV (B V norm f) <= c"; 
-  proof (rule ub_ge_sup);
+  proof (rule sup_le_ub);
     from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
       by (simp! add: is_function_norm_def function_norm_def); 
     show "isUb UNIV (B V norm f) c";  
     proof (intro isUbI setleI ballI);
       fix y; assume "y: B V norm f";

           by (simp! add: order_less_imp_not_eq);
         qed;
             
 	from lt; have "0r < rinv (norm x)";
 	  by (simp! add: real_rinv_gt_zero);
-	then; have inv_leq: "0r <= rinv (norm x)"; by (rule less_imp_le);
+	then; have inv_leq: "0r <= rinv (norm x)"; by (rule real_less_imp_le);
 
 	from Px; have "y = rabs (f x) * rinv (norm x)"; ..;
 	also; from inv_leq; have "... <= c * norm x * rinv (norm x)";
 	  proof (rule real_mult_le_le_mono2);
 	    from fb x; show "rabs (f x) <= c * norm x"; ..;