src/HOL/Real/HahnBanach/HahnBanach.thy

               have "H <= E"; ..;
               thus "H < E"; ..;
             qed;
             thus ?thesis; by blast;
           qed;
-          have x0: "x0 ~= <0>";
+          have x0: "x0 ~= 00";
           proof (rule classical);
-            presume "x0 = <0>";
+            presume "x0 = 00";
             with h; have "x0:H"; by simp;
             thus ?thesis; by contradiction;
           qed blast;
 
 txt {* Define $H_0$ as the direct sum of $H$ and the linear closure of $x_0$.  *};

               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 
+            def h0 == "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a (*) x0 
                                                   & y:H
                            in (h y) + a * xi";
             show ?thesis;
             proof;
  

 		show "g <= graph H0 h0";
 		proof -;
 		  have  "graph H h <= graph H0 h0";
                   proof (rule graph_extI);
 		    fix t; assume "t:H"; 
-		    have "(SOME (y, a). t = y + a <*> x0 & y : H)
+		    have "(SOME (y, a). t = y + a (*) x0 & y : H)
                          = (t,0r)";
 		      by (rule decomp_H0_H [OF _ _ _ _ _ x0]);
 		    thus "h t = h0 t"; by (simp! add: Let_def);
 		  next;
 		    show "H <= H0";

 		  have "graph H h ~= graph H0 h0";
 		  proof;
 		    assume e: "graph H h = graph H0 h0";
 		    have "x0 : H0"; 
 		    proof (unfold H0_def, rule vs_sumI);
-		      show "x0 = <0> + x0"; by (simp!);
-		      from h; show "<0> : H"; ..;
+		      show "x0 = 00 + x0"; by (simp!);
+		      from h; show "00 : H"; ..;
 		      show "x0 : lin x0"; by (rule x_lin_x);
 		    qed;
 		    hence "(x0, h0 x0) : graph H0 h0"; ..;
 		    with e; have "(x0, h0 x0) : graph H h"; by simp;
 		    hence "x0 : H"; ..;

 		    have "f x = h x"; ..;
 		    also; have " ... = h x + 0r * xi"; by simp;
 		    also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
 		      by (simp add: Let_def);
 		    also; have 
-		      "(x, 0r) = (SOME (y, a). x = y + a <*> x0 & y : H)";
+		      "(x, 0r) = (SOME (y, a). x = y + a (*) x0 & y : H)";
 		      by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x0]) (simp!)+;
 		    also; have 
-		      "(let (y,a) = (SOME (y,a). x = y + a <*> x0 & y : H)
+		      "(let (y,a) = (SOME (y,a). x = y + a (*) x0 & y : H)
                         in h y + a * xi) 
                       = h0 x"; by (simp!);
 		    finally; show "f x = h0 x"; .;
 		  next;
 		    from f_h0; show "F <= H0"; ..;

   hence "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 
                  & graph H0 h0 : M";
   proof;
     fix x0; assume "x0:E" "x0~:H";
 
-    have x0: "x0 ~= <0>";
+    have x0: "x0 ~= 00";
     proof (rule classical);
-      presume "x0 = <0>";
+      presume "x0 = 00";
       with h; have "x0:H"; by simp;
       thus ?thesis; by contradiction;
     qed blast;
 
     txt {* Define $H_0$ as the (direct) sum of H and the 

      
       txt {* Define $h_0$ as the canonical linear extension 
       of $h$ on $H_0$:*};  
 
       def h0 ==
-          "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 & y:H
+          "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a ( * ) x0 & y:H
                in (h y) + a * xi";
 
       txt {* We get that the graph of $h_0$ extends that of
       $h$. *};
         
       have  "graph H h <= graph H0 h0"; 
       proof (rule graph_extI);
         fix t; assume "t:H"; 
-        have "(SOME (y, a). t = y + a <*> x0 & y : H) = (t,0r)";
+        have "(SOME (y, a). t = y + a ( * ) x0 & y : H) = (t,0r)";
           by (rule decomp_H0_H, rule x0); 
         thus "h t = h0 t"; by (simp! add: Let_def);
       next;
         show "H <= H0";
         proof (rule subspace_subset);

       have "graph H h ~= graph H0 h0";
       proof;
         assume e: "graph H h = graph H0 h0";
         have "x0 : H0"; 
         proof (unfold H0_def, rule vs_sumI);
-          show "x0 = <0> + x0"; by (simp!);
-          from h; show "<0> : H"; ..;
+          show "x0 = 00 + x0"; by (simp!);
+          from h; show "00 : H"; ..;
           show "x0 : lin x0"; by (rule x_lin_x);
         qed;
         hence "(x0, h0 x0) : graph H0 h0"; ..;
         with e; have "(x0, h0 x0) : graph H h"; by simp;
         hence "x0 : H"; ..;

           have "f x = h x"; ..;
           also; have " ... = h x + 0r * xi"; by simp;
           also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
             by (simp add: Let_def);
           also; have 
-            "(x, 0r) = (SOME (y, a). x = y + a <*> x0 & y : H)";
+            "(x, 0r) = (SOME (y, a). x = y + a ( * ) x0 & y : H)";
             by (rule decomp_H0_H [RS sym], rule x0) (simp!)+;
           also; have 
-            "(let (y,a) = (SOME (y,a). x = y + a <*> x0 & y : H)
+            "(let (y,a) = (SOME (y,a). x = y + a ( * ) x0 & y : H)
               in h y + a * xi) 
              = h0 x"; by (simp!);
           finally; show "f x = h0 x"; .;
         next;
           from f_h0; show "F <= H0"; ..;

       show "0r <= norm x"; ..;
     qed;
 
     txt{* $p$ is absolutely homogenous: *};
 
-    show "p (a <*> x) = rabs a * p x";
+    show "p (a (*) x) = rabs a * p x";
     proof -; 
-      have "p (a <*> x) = function_norm F norm f * norm (a <*> x)";
+      have "p (a (*) x) = function_norm F norm f * norm (a (*) x)";
         by (simp!);
-      also; have "norm (a <*> x) = rabs a * norm x"; 
+      also; have "norm (a (*) x) = rabs a * norm x"; 
         by (rule normed_vs_norm_rabs_homogenous);
       also; have "function_norm F norm f * (rabs a * norm x) 
         = rabs a * (function_norm F norm f * norm x)";
         by (simp! only: real_mult_left_commute);
       also; have "... = rabs a * p x"; by (simp!);