# HG changeset patch
# User nipkow
# Date 955630910 -7200
# Node ID 816d8f6513be7c13deef760caa86d8897f811b23
# Parent  78b7010db84792ae402e534dfe95ba9a9c6a3b90
Times -> <*>
**    -> <*lex*>

diff -r 78b7010db847 -r 816d8f6513be src/HOL/BCV/SemiLattice.ML
--- a/src/HOL/BCV/SemiLattice.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/BCV/SemiLattice.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -150,6 +150,6 @@
 
 (* product *)
 
-Goalw [semilat_def,plus_prod] "[| semilat A; semilat B |] ==> semilat (A Times B)";
+Goalw [semilat_def,plus_prod] "[| semilat A; semilat B |] ==> semilat (A <*> B)";
 by (Asm_simp_tac 1);
 qed "semilat_Times";
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Induct/LList.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -616,20 +616,20 @@
 (*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
 
 Goalw [LListD_Fun_def]
-    "r <= (llist A) Times (llist A) ==> \
-\           LListD_Fun (diag A) r <= (llist A) Times (llist A)";
+    "r <= (llist A) <*> (llist A) ==> \
+\           LListD_Fun (diag A) r <= (llist A) <*> (llist A)";
 by (stac llist_unfold 1);
 by (simp_tac (simpset() addsimps [NIL_def, CONS_def]) 1);
 by (Fast_tac 1);
 qed "LListD_Fun_subset_Times_llist";
 
 Goal "prod_fun Rep_LList Rep_LList `` r <= \
-\    (llist(range Leaf)) Times (llist(range Leaf))";
+\    (llist(range Leaf)) <*> (llist(range Leaf))";
 by (fast_tac (claset() delrules [image_subsetI]
 		       addIs [Rep_LList RS LListD]) 1);
 qed "subset_Times_llist";
 
-Goal "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
+Goal "r <= (llist(range Leaf)) <*> (llist(range Leaf)) ==> \
 \    prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) `` r <= r";
 by Safe_tac;
 by (etac (subsetD RS SigmaE2) 1);
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Induct/Mutil.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -32,22 +32,22 @@
 Addsimps [below_0];
 
 Goalw [below_def]
-    "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
+    "below(Suc n) <*> B = ({n} <*> B) Un ((below n) <*> B)";
 by Auto_tac;
 qed "Sigma_Suc1";
 
 Goalw [below_def]
-    "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
+    "A <*> below(Suc n) = (A <*> {n}) Un (A <*> (below n))";
 by Auto_tac;
 qed "Sigma_Suc2";
 
 Addsimps [Sigma_Suc1, Sigma_Suc2];
 
-Goal "({i} Times {n}) Un ({i} Times {m}) = {(i,m), (i,n)}";
+Goal "({i} <*> {n}) Un ({i} <*> {m}) = {(i,m), (i,n)}";
 by Auto_tac;
 qed "sing_Times_lemma";
 
-Goal "{i} Times below(n+n) : tiling domino";
+Goal "{i} <*> below(n+n) : tiling domino";
 by (induct_tac "n" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym])));
 by (rtac tiling.Un 1);
@@ -56,7 +56,7 @@
 
 AddSIs [dominoes_tile_row]; 
 
-Goal "(below m) Times below(n+n) : tiling domino";
+Goal "(below m) <*> below(n+n) : tiling domino";
 by (induct_tac "m" 1);
 by Auto_tac;
 qed "dominoes_tile_matrix";
@@ -121,7 +121,7 @@
 qed "gen_mutil_not_tiling";
 
 (*Apply the general theorem to the well-known case*)
-Goal "[| t = below(Suc m + Suc m) Times below(Suc n + Suc n) |] \
+Goal "[| t = below(Suc m + Suc m) <*> below(Suc n + Suc n) |] \
 \     ==> t - {(0,0)} - {(Suc(m+m), Suc(n+n))} ~: tiling domino";
 by (rtac gen_mutil_not_tiling 1);
 by (blast_tac (claset() addSIs [dominoes_tile_matrix]) 1);
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Integ/Equiv.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -73,7 +73,7 @@
 qed "equiv_class_nondisjoint";
 
 val [major] = goalw Equiv.thy [equiv_def,refl_def]
-    "equiv A r ==> r <= A Times A";
+    "equiv A r ==> r <= A <*> A";
 by (rtac (major RS conjunct1 RS conjunct1) 1);
 qed "equiv_type";
 
@@ -241,8 +241,8 @@
 
 (*** Cardinality results suggested by Florian Kammueller ***)
 
-(*Recall that  equiv A r  implies  r <= A Times A   (equiv_type) *)
-Goal "[| finite A; r <= A Times A |] ==> finite (A/r)";
+(*Recall that  equiv A r  implies  r <= A <*> A   (equiv_type) *)
+Goal "[| finite A; r <= A <*> A |] ==> finite (A/r)";
 by (rtac finite_subset 1);
 by (etac (finite_Pow_iff RS iffD2) 2);
 by (rewtac quotient_def);
@@ -250,7 +250,7 @@
 qed "finite_quotient";
 
 Goalw [quotient_def]
-    "[| finite A;  r <= A Times A;  X : A/r |] ==> finite X";
+    "[| finite A;  r <= A <*> A;  X : A/r |] ==> finite X";
 by (rtac finite_subset 1);
 by (assume_tac 2);
 by (Blast_tac 1);
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -67,11 +67,11 @@
   by (simp add: below_def);
 
 lemma Sigma_Suc1:
-    "below (Suc n) Times B = ({n} Times B) Un (below n Times B)";
+    "below (Suc n) <*> B = ({n} <*> B) Un (below n <*> B)";
   by (simp add: below_def less_Suc_eq) blast;
 
 lemma Sigma_Suc2:
-    "A Times below (Suc n) = (A Times {n}) Un (A Times (below n))";
+    "A <*> below (Suc n) = (A <*> {n}) Un (A <*> (below n))";
   by (simp add: below_def less_Suc_eq) blast;
 
 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2;
@@ -122,13 +122,13 @@
     vertl:  "{(i, j), (i + 1, j)} : domino";
 
 lemma dominoes_tile_row:
-  "{i} Times below (2 * n) : tiling domino"
+  "{i} <*> below (2 * n) : tiling domino"
   (is "?P n" is "?B n : ?T");
 proof (induct n);
   show "?P 0"; by (simp add: below_0 tiling.empty);
 
   fix n; assume hyp: "?P n";
-  let ?a = "{i} Times {2 * n + 1} Un {i} Times {2 * n}";
+  let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}";
 
   have "?B (Suc n) = ?a Un ?B n"; by (simp add: Sigma_Suc Un_assoc);
   also; have "... : ?T";
@@ -144,13 +144,13 @@
 qed;
 
 lemma dominoes_tile_matrix:
-  "below m Times below (2 * n) : tiling domino"
+  "below m <*> below (2 * n) : tiling domino"
   (is "?P m" is "?B m : ?T");
 proof (induct m);
   show "?P 0"; by (simp add: below_0 tiling.empty);
 
   fix m; assume hyp: "?P m";
-  let ?t = "{m} Times below (2 * n)";
+  let ?t = "{m} <*> below (2 * n)";
 
   have "?B (Suc m) = ?t Un ?B m"; by (simp add: Sigma_Suc);
   also; have "... : ?T";
@@ -249,13 +249,13 @@
 constdefs
   mutilated_board :: "nat => nat => (nat * nat) set"
   "mutilated_board m n ==
-    below (2 * (m + 1)) Times below (2 * (n + 1))
+    below (2 * (m + 1)) <*> below (2 * (n + 1))
       - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}";
 
 theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino";
 proof (unfold mutilated_board_def);
   let ?T = "tiling domino";
-  let ?t = "below (2 * (m + 1)) Times below (2 * (n + 1))";
+  let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))";
   let ?t' = "?t - {(0, 0)}";
   let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}";
 
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Lex/AutoChopper1.thy
--- a/src/HOL/Lex/AutoChopper1.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Lex/AutoChopper1.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -22,7 +22,7 @@
 consts
   acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)
           => 'a list list * 'a list"
-recdef acc "inv_image (less_than ** less_than)
+recdef acc "inv_image (less_than <*lex*> less_than)
               (%(A,ys,s,xss,zs,xs). (length xs + length ys + length zs,
                                      length ys))"
 "acc(A,[],s,xss,zs,[]) = (xss, zs)"
diff -r 78b7010db847 -r 816d8f6513be src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/List.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -176,7 +176,7 @@
  lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
 primrec
 "lexn r 0       = {}"
-"lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r ** lexn r n)) Int
+"lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r <*lex*> lexn r n)) Int
                   {(xs,ys). length xs = Suc n & length ys = Suc n}"
 
 constdefs
@@ -184,7 +184,7 @@
 "lex r == UN n. lexn r n"
 
  lexico :: "('a * 'a)set => ('a list * 'a list)set"
-"lexico r == inv_image (less_than ** lex r) (%xs. (length xs, xs))"
+"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
 
 end
 
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Prod.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -401,22 +401,37 @@
 by (Blast_tac 1) ;
 qed "Sigma_empty1";
 
-Goal "A Times {} = {}";
+Goal "A <*> {} = {}";
 by (Blast_tac 1) ;
 qed "Sigma_empty2";
 
-Addsimps [Sigma_empty1,Sigma_empty2]; 
+Addsimps [Sigma_empty1,Sigma_empty2];
+
+Goal "UNIV <*> UNIV = UNIV";
+by Auto_tac;
+qed "UNIV_Times_UNIV"; 
+Addsimps [UNIV_Times_UNIV];
+
+Goal "- (UNIV <*> A) = UNIV <*> (-A)";
+by Auto_tac;
+qed "Compl_Times_UNIV1"; 
+
+Goal "- (A <*> UNIV) = (-A) <*> UNIV";
+by Auto_tac;
+qed "Compl_Times_UNIV2"; 
+
+Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; 
 
 Goal "((a,b): Sigma A B) = (a:A & b:B(a))";
 by (Blast_tac 1);
 qed "mem_Sigma_iff";
 AddIffs [mem_Sigma_iff]; 
 
-Goal "x:C ==> (A Times C <= B Times C) = (A <= B)";
+Goal "x:C ==> (A <*> C <= B <*> C) = (A <= B)";
 by (Blast_tac 1);
 qed "Times_subset_cancel2";
 
-Goal "x:C ==> (A Times C = B Times C) = (A = B)";
+Goal "x:C ==> (A <*> C = B <*> C) = (A = B)";
 by (blast_tac (claset() addEs [equalityE]) 1);
 qed "Times_eq_cancel2";
 
@@ -426,14 +441,14 @@
 
 (*** Complex rules for Sigma ***)
 
-Goal "{(a,b). P a & Q b} = Collect P Times Collect Q";
+Goal "{(a,b). P a & Q b} = Collect P <*> Collect Q";
 by (Blast_tac 1);
 qed "Collect_split";
 
 Addsimps [Collect_split];
 
 (*Suggested by Pierre Chartier*)
-Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
+Goal "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)";
 by (Blast_tac 1);
 qed "UN_Times_distrib";
 
@@ -477,15 +492,15 @@
 
 (*Non-dependent versions are needed to avoid the need for higher-order
   matching, especially when the rules are re-oriented*)
-Goal "(A Un B) Times C = (A Times C) Un (B Times C)";
+Goal "(A Un B) <*> C = (A <*> C) Un (B <*> C)";
 by (Blast_tac 1);
 qed "Times_Un_distrib1"; 
 
-Goal "(A Int B) Times C = (A Times C) Int (B Times C)";
+Goal "(A Int B) <*> C = (A <*> C) Int (B <*> C)";
 by (Blast_tac 1);
 qed "Times_Int_distrib1"; 
 
-Goal "(A - B) Times C = (A Times C) - (B Times C)";
+Goal "(A - B) <*> C = (A <*> C) - (B <*> C)";
 by (Blast_tac 1);
 qed "Times_Diff_distrib1"; 
 
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Prod.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -55,7 +55,7 @@
   "_patterns"   :: [pttrn, patterns] => patterns ("_,/_")
 
   "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
-  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ Times _" [81, 80] 80)
+  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    (infixr "<*>" 80)
 
 translations
   "(x, y, z)"    == "(x, (y, z))"
@@ -68,7 +68,7 @@
      The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
 
   "SIGMA x:A. B" => "Sigma A (%x. B)"
-  "A Times B"    => "Sigma A (_K B)"
+  "A <*> B"      => "Sigma A (_K B)"
 
 syntax (symbols)
   "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -66,7 +66,7 @@
 constdefs
   B :: "[ 'a set, 'a => real, 'a => real ] => real set"
   "B V norm f == 
-  {0r} \Un {rabs (f x) * rinv (norm x) | x. x ~= <0> & x:V}";
+  {0r} \Un {rabs (f x) * rinv (norm x) | x. x ~= 00 & x:V}";
 
 text{* $n$ is the function norm of $f$, iff 
 $n$ is the supremum of $B$. 
@@ -141,7 +141,7 @@
 
       next;
 	fix x y;
-        assume "x:V" "x ~= <0>"; (***
+        assume "x:V" "x ~= 00"; (***
 
          have ge: "0r <= rinv (norm x)";
           by (rule real_less_imp_le, rule real_rinv_gt_zero, 
@@ -207,7 +207,7 @@
     proof (intro ballI, unfold B_def,
            elim UnE singletonE CollectE exE conjE); 
       fix x r;
-      assume "x : V" "x ~= <0>" 
+      assume "x : V" "x ~= 00" 
         and r: "r = rabs (f x) * rinv (norm x)";
 
       have ge: "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero);
@@ -259,9 +259,9 @@
     from the linearity of $f$: for every linear function
     holds $f\ap \zero = 0$. *};
 
-    assume "x = <0>";
-    have "rabs (f x) = rabs (f <0>)"; by (simp!);
-    also; from v continuous_linearform; have "f <0> = 0r"; ..;
+    assume "x = 00";
+    have "rabs (f x) = rabs (f 00)"; by (simp!);
+    also; from v continuous_linearform; have "f 00 = 0r"; ..;
     also; note rabs_zero;
     also; have "0r <= function_norm V norm f * norm x";
     proof (rule real_le_mult_order);
@@ -272,7 +272,7 @@
     show "rabs (f x) <= function_norm V norm f * norm x"; .;
 
   next;
-    assume "x ~= <0>";
+    assume "x ~= 00";
     have n: "0r <= norm x"; ..;
     have nz: "norm x ~= 0r";
     proof (rule lt_imp_not_eq [RS not_sym]);
@@ -356,7 +356,7 @@
 
       next;
 	fix x; 
-        assume "x : V" "x ~= <0>"; 
+        assume "x : V" "x ~= 00"; 
 
         have lz: "0r < norm x"; 
           by (simp! add: normed_vs_norm_gt_zero);
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -145,9 +145,9 @@
             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;
@@ -190,7 +190,7 @@
 
 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;
@@ -205,7 +205,7 @@
 		  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);
@@ -228,8 +228,8 @@
 		    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"; ..;
@@ -265,10 +265,10 @@
 		    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"; .;
@@ -427,9 +427,9 @@
   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;
@@ -471,7 +471,7 @@
       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
@@ -480,7 +480,7 @@
       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;
@@ -502,8 +502,8 @@
         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"; ..;
@@ -545,10 +545,10 @@
           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"; .;
@@ -672,11 +672,11 @@
 
     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)";
@@ -801,4 +801,4 @@
   qed;
 qed;
 
-end;
\ No newline at end of file
+end;
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -52,27 +52,27 @@
   
     txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
 
-    from vs; have "a <0> : ?S"; by force;
+    from vs; have "a 00 : ?S"; by force;
     thus "EX X. X : ?S"; ..;
 
     txt {* $b\ap \zero$ is an upper bound of $S$: *};
 
     show "EX Y. isUb UNIV ?S Y"; 
     proof; 
-      show "isUb UNIV ?S (b <0>)";
+      show "isUb UNIV ?S (b 00)";
       proof (intro isUbI setleI ballI);
-        show "b <0> : UNIV"; ..;
+        show "b 00 : UNIV"; ..;
       next;
 
         txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
 
         fix y; assume y: "y : ?S"; 
         from y; have "EX u:F. y = a u"; by fast;
-        thus "y <= b <0>"; 
+        thus "y <= b 00"; 
         proof;
           fix u; assume "u:F"; 
           assume "y = a u";
-          also; have "a u <= b <0>"; by (rule r) (simp!)+;
+          also; have "a u <= b 00"; by (rule r) (simp!)+;
           finally; show ?thesis; .;
         qed;
       qed;
@@ -121,18 +121,18 @@
 is a linear extension of $h$ to $H_0$. *};
 
 lemma h0_lf: 
-  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
+  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H 
                 in h y + a * xi);
   H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H; 
-  x0 : E; x0 ~= <0>; is_vectorspace E |]
+  x0 : E; x0 ~= 00; is_vectorspace E |]
   ==> is_linearform H0 h0";
 proof -;
   assume h0_def: 
-    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
+    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H 
                in h y + a * xi)"
     and H0_def: "H0 == H + lin x0" 
     and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
-      "x0 ~= <0>" "x0 : E" "is_vectorspace E";
+      "x0 ~= 00" "x0 : E" "is_vectorspace E";
 
   have h0: "is_vectorspace H0"; 
   proof (unfold H0_def, rule vs_sum_vs);
@@ -150,27 +150,27 @@
     have x1x2: "x1 + x2 : H0"; 
       by (rule vs_add_closed, rule h0); 
     from x1; 
-    have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0  & y1 : H"; 
+    have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0  & y1 : H"; 
       by (unfold H0_def vs_sum_def lin_def) fast;
     from x2; 
-    have ex_x2: "EX y2 a2. x2 = y2 + a2 <*> x0 & y2 : H"; 
+    have ex_x2: "EX y2 a2. x2 = y2 + a2 (*) x0 & y2 : H"; 
       by (unfold H0_def vs_sum_def lin_def) fast;
     from x1x2; 
-    have ex_x1x2: "EX y a. x1 + x2 = y + a <*> x0 & y : H";
+    have ex_x1x2: "EX y a. x1 + x2 = y + a (*) x0 & y : H";
       by (unfold H0_def vs_sum_def lin_def) fast;
 
     from ex_x1 ex_x2 ex_x1x2;
     show "h0 (x1 + x2) = h0 x1 + h0 x2";
     proof (elim exE conjE);
       fix y1 y2 y a1 a2 a;
-      assume y1: "x1 = y1 + a1 <*> x0"     and y1': "y1 : H"
-         and y2: "x2 = y2 + a2 <*> x0"     and y2': "y2 : H" 
-         and y: "x1 + x2 = y + a <*> x0"   and y':  "y  : H"; 
+      assume y1: "x1 = y1 + a1 (*) x0"     and y1': "y1 : H"
+         and y2: "x2 = y2 + a2 (*) x0"     and y2': "y2 : H" 
+         and y: "x1 + x2 = y + a (*) x0"   and y':  "y  : H"; 
 
       have ya: "y1 + y2 = y & a1 + a2 = a"; 
       proof (rule decomp_H0);;
 	txt_raw {* \label{decomp-H0-use} *};;
-        show "y1 + y2 + (a1 + a2) <*> x0 = y + a <*> x0"; 
+        show "y1 + y2 + (a1 + a2) (*) x0 = y + a (*) x0"; 
           by (simp! add: vs_add_mult_distrib2 [of E]);
         show "y1 + y2 : H"; ..;
       qed;
@@ -199,31 +199,31 @@
 
   next;  
     fix c x1; assume x1: "x1 : H0";    
-    have ax1: "c <*> x1 : H0";
+    have ax1: "c (*) x1 : H0";
       by (rule vs_mult_closed, rule h0);
     from x1; have ex_x: "!! x. x: H0 
-                        ==> EX y a. x = y + a <*> x0 & y : H";
+                        ==> EX y a. x = y + a (*) x0 & y : H";
       by (unfold H0_def vs_sum_def lin_def) fast;
 
-    from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
+    from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H";
       by (unfold H0_def vs_sum_def lin_def) fast;
-    with ex_x [of "c <*> x1", OF ax1];
-    show "h0 (c <*> x1) = c * (h0 x1)";  
+    with ex_x [of "c (*) x1", OF ax1];
+    show "h0 (c (*) x1) = c * (h0 x1)";  
     proof (elim exE conjE);
       fix y1 y a1 a; 
-      assume y1: "x1 = y1 + a1 <*> x0"       and y1': "y1 : H"
-        and y: "c <*> x1 = y  + a  <*> x0"   and y':  "y  : H"; 
+      assume y1: "x1 = y1 + a1 (*) x0"       and y1': "y1 : H"
+        and y: "c (*) x1 = y  + a  (*) x0"   and y':  "y  : H"; 
 
-      have ya: "c <*> y1 = y & c * a1 = a"; 
+      have ya: "c (*) y1 = y & c * a1 = a"; 
       proof (rule decomp_H0); 
-	show "c <*> y1 + (c * a1) <*> x0 = y + a <*> x0"; 
+	show "c (*) y1 + (c * a1) (*) x0 = y + a (*) x0"; 
           by (simp! add: add: vs_add_mult_distrib1);
-        show "c <*> y1 : H"; ..;
+        show "c (*) y1 : H"; ..;
       qed;
 
-      have "h0 (c <*> x1) = h y + a * xi"; 
+      have "h0 (c (*) x1) = h y + a * xi"; 
 	by (rule h0_definite);
-      also; have "... = h (c <*> y1) + (c * a1) * xi";
+      also; have "... = h (c (*) y1) + (c * a1) * xi";
         by (simp add: ya);
       also; from vs y1'; have "... = c * h y1 + c * a1 * xi"; 
 	by (simp add: linearform_mult [of H]);
@@ -240,31 +240,31 @@
 is bounded by the seminorm $p$. *};
 
 lemma h0_norm_pres:
-  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
+  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H 
                 in h y + a * xi);
-  H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E; 
+  H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= 00; is_vectorspace E; 
   is_subspace H E; is_seminorm E p; is_linearform H h; ALL y:H. h y <= p y; 
   ALL y:H. - p (y + x0) - h y <= xi & xi <= p (y + x0) - h y |]
    ==> ALL x:H0. h0 x <= p x"; 
 proof; 
   assume h0_def: 
-    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
+    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H 
                in (h y) + a * xi)"
     and H0_def: "H0 == H + lin x0" 
-    and vs: "x0 ~: H" "x0 : E" "x0 ~= <0>" "is_vectorspace E" 
+    and vs: "x0 ~: H" "x0 : E" "x0 ~= 00" "is_vectorspace E" 
             "is_subspace H E" "is_seminorm E p" "is_linearform H h" 
     and a: "ALL y:H. h y <= p y";
   presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi";
   presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya";
   fix x; assume "x : H0"; 
   have ex_x: 
-    "!! x. x : H0 ==> EX y a. x = y + a <*> x0 & y : H";
+    "!! x. x : H0 ==> EX y a. x = y + a (*) x0 & y : H";
     by (unfold H0_def vs_sum_def lin_def) fast;
-  have "EX y a. x = y + a <*> x0 & y : H";
+  have "EX y a. x = y + a (*) x0 & y : H";
     by (rule ex_x);
   thus "h0 x <= p x";
   proof (elim exE conjE);
-    fix y a; assume x: "x = y + a <*> x0" and y: "y : H";
+    fix y a; assume x: "x = y + a (*) x0" and y: "y : H";
     have "h0 x = h y + a * xi";
       by (rule h0_definite);
 
@@ -272,7 +272,7 @@
     $h\ap y + a \cdot \xi\leq  p\ap (y\plus a \mult x_0)$ 
     by case analysis on $a$. \label{linorder_linear_split}*};
 
-    also; have "... <= p (y + a <*> x0)";
+    also; have "... <= p (y + a (*) x0)";
     proof (rule linorder_linear_split); 
 
       assume z: "a = 0r"; 
@@ -284,27 +284,27 @@
     next;
       assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
       from a1; 
-      have "- p (rinv a <*> y + x0) - h (rinv a <*> y) <= xi";
+      have "- p (rinv a (*) y + x0) - h (rinv a (*) y) <= xi";
         by (rule bspec) (simp!);
 
       txt {* The thesis for this case now follows by a short  
       calculation. *};      
       hence "a * xi 
-            <= a * (- p (rinv a <*> y + x0) - h (rinv a <*> y))";
+            <= a * (- p (rinv a (*) y + x0) - h (rinv a (*) y))";
         by (rule real_mult_less_le_anti [OF lz]);
-      also; have "... = - a * (p (rinv a <*> y + x0)) 
-                        - a * (h (rinv a <*> y))";
+      also; have "... = - a * (p (rinv a (*) y + x0)) 
+                        - a * (h (rinv a (*) y))";
         by (rule real_mult_diff_distrib);
-      also; from lz vs y; have "- a * (p (rinv a <*> y + x0)) 
-                               = p (a <*> (rinv a <*> y + x0))";
+      also; from lz vs y; have "- a * (p (rinv a (*) y + x0)) 
+                               = p (a (*) (rinv a (*) y + x0))";
         by (simp add: seminorm_rabs_homogenous rabs_minus_eqI2);
-      also; from nz vs y; have "... = p (y + a <*> x0)";
+      also; from nz vs y; have "... = p (y + a (*) x0)";
         by (simp add: vs_add_mult_distrib1);
-      also; from nz vs y; have "a * (h (rinv a <*> y)) =  h y";
+      also; from nz vs y; have "a * (h (rinv a (*) y)) =  h y";
         by (simp add: linearform_mult [RS sym]);
-      finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
+      finally; have "a * xi <= p (y + a (*) x0) - h y"; .;
 
-      hence "h y + a * xi <= h y + p (y + a <*> x0) - h y";
+      hence "h y + a * xi <= h y + p (y + a (*) x0) - h y";
         by (simp add: real_add_left_cancel_le);
       thus ?thesis; by simp;
 
@@ -314,30 +314,30 @@
     next; 
       assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
       from a2;
-      have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
+      have "xi <= p (rinv a (*) y + x0) - h (rinv a (*) y)";
         by (rule bspec) (simp!);
 
       txt {* The thesis for this case follows by a short
       calculation: *};
 
       with gz; have "a * xi 
-            <= a * (p (rinv a <*> y + x0) - h (rinv a <*> y))";
+            <= a * (p (rinv a (*) y + x0) - h (rinv a (*) y))";
         by (rule real_mult_less_le_mono);
-      also; have "... = a * p (rinv a <*> y + x0) 
-                        - a * h (rinv a <*> y)";
+      also; have "... = a * p (rinv a (*) y + x0) 
+                        - a * h (rinv a (*) y)";
         by (rule real_mult_diff_distrib2); 
       also; from gz vs y; 
-      have "a * p (rinv a <*> y + x0) 
-           = p (a <*> (rinv a <*> y + x0))";
+      have "a * p (rinv a (*) y + x0) 
+           = p (a (*) (rinv a (*) y + x0))";
         by (simp add: seminorm_rabs_homogenous rabs_eqI2);
       also; from nz vs y; 
-      have "... = p (y + a <*> x0)";
+      have "... = p (y + a (*) x0)";
         by (simp add: vs_add_mult_distrib1);
-      also; from nz vs y; have "a * h (rinv a <*> y) = h y";
+      also; from nz vs y; have "a * h (rinv a (*) y) = h y";
         by (simp add: linearform_mult [RS sym]); 
-      finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
+      finally; have "a * xi <= p (y + a (*) x0) - h y"; .;
  
-      hence "h y + a * xi <= h y + (p (y + a <*> x0) - h y)";
+      hence "h y + a * xi <= h y + (p (y + a (*) x0) - h y)";
         by (simp add: real_add_left_cancel_le);
       thus ?thesis; by simp;
     qed;
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -437,16 +437,16 @@
 
     txt{* We have to show that $h$ is multiplicative. *};
 
-    thus "h (a <*> x) = a * h x";
+    thus "h (a (*) x) = a * h x";
     proof (elim exE conjE);
       fix H' h'; assume "x:H'"
         and b: "graph H' h' <= graph H h" 
         and "is_linearform H' h'" "is_subspace H' E";
-      have "h' (a <*> x) = a * h' x"; 
+      have "h' (a (*) x) = a * h' x"; 
         by (rule linearform_mult);
       also; have "h' x = h x"; ..;
-      also; have "a <*> x : H'"; ..;
-      with b; have "h' (a <*> x) = h (a <*> x)"; ..;
+      also; have "a (*) x : H'"; ..;
+      with b; have "h' (a (*) x) = h (a (*) x)"; ..;
       finally; show ?thesis; .;
     qed;
   qed;
@@ -507,7 +507,7 @@
 
   show ?thesis; 
   proof;
-    show "<0> : F"; ..;
+    show "00 : F"; ..;
     show "F <= H"; 
     proof (rule graph_extD2);
       show "graph F f <= graph H h";
@@ -518,10 +518,10 @@
       fix x y; assume "x:F" "y:F";
       show "x + y : F"; by (simp!);
     qed;
-    show "ALL x:F. ALL a. a <*> x : F";
+    show "ALL x:F. ALL a. a (*) x : F";
     proof (intro ballI allI);
       fix x a; assume "x:F";
-      show "a <*> x : F"; by (simp!);
+      show "a (*) x : F"; by (simp!);
     qed;
   qed;
 qed;
@@ -542,10 +542,10 @@
     txt {* The $\zero$ element is in $H$, as $F$ is a subset 
     of $H$: *};
 
-    have "<0> : F"; ..;
+    have "00 : F"; ..;
     also; have "is_subspace F H"; by (rule sup_supF); 
     hence "F <= H"; ..;
-    finally; show "<0> : H"; .;
+    finally; show "00 : H"; .;
 
     txt{* $H$ is a subset of $E$: *};
 
@@ -588,7 +588,7 @@
 
     txt{* $H$ is closed under scalar multiplication: *};
 
-    show "ALL x:H. ALL a. a <*> x : H"; 
+    show "ALL x:H. ALL a. a (*) x : H"; 
     proof (intro ballI allI); 
       fix x a; assume "x:H"; 
       have "EX H' h'. x:H' & graph H' h' <= graph H h
@@ -596,11 +596,11 @@
               & is_subspace F H' & graph F f <= graph H' h' 
               & (ALL x:H'. h' x <= p x)"; 
 	by (rule some_H'h'); 
-      thus "a <*> x : H"; 
+      thus "a (*) x : H"; 
       proof (elim exE conjE);
 	fix H' h'; 
         assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
-        have "a <*> x : H'"; ..;
+        have "a (*) x : H'"; ..;
         also; have "H' <= H"; ..;
 	finally; show ?thesis; .;
       qed;
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -14,11 +14,11 @@
   is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" 
   "is_linearform V f == 
       (ALL x: V. ALL y: V. f (x + y) = f x + f y) &
-      (ALL x: V. ALL a. f (a <*> x) = a * (f x))"; 
+      (ALL x: V. ALL a. f (a (*) x) = a * (f x))"; 
 
 lemma is_linearformI [intro]: 
   "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y;
-    !! x c. x : V ==> f (c <*> x) = c * f x |]
+    !! x c. x : V ==> f (c (*) x) = c * f x |]
  ==> is_linearform V f";
  by (unfold is_linearform_def) force;
 
@@ -27,7 +27,7 @@
   by (unfold is_linearform_def) fast;
 
 lemma linearform_mult [intro??]: 
-  "[| is_linearform V f; x:V |] ==>  f (a <*> x) = a * (f x)"; 
+  "[| is_linearform V f; x:V |] ==>  f (a (*) x) = a * (f x)"; 
   by (unfold is_linearform_def) fast;
 
 lemma linearform_neg [intro??]:
@@ -35,7 +35,7 @@
   ==> f (- x) = - f x";
 proof -; 
   assume "is_linearform V f" "is_vectorspace V" "x:V"; 
-  have "f (- x) = f ((- 1r) <*> x)"; by (simp! add: negate_eq1);
+  have "f (- x) = f ((- 1r) (*) x)"; by (simp! add: negate_eq1);
   also; have "... = (- 1r) * (f x)"; by (rule linearform_mult);
   also; have "... = - (f x)"; by (simp!);
   finally; show ?thesis; .;
@@ -56,14 +56,14 @@
 text{* Every linear form yields $0$ for the $\zero$ vector.*};
 
 lemma linearform_zero [intro??, simp]: 
-  "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
+  "[| is_vectorspace V; is_linearform V f |] ==> f 00 = 0r"; 
 proof -; 
   assume "is_vectorspace V" "is_linearform V f";
-  have "f <0> = f (<0> - <0>)"; by (simp!);
-  also; have "... = f <0> - f <0>"; 
+  have "f 00 = f (00 - 00)"; by (simp!);
+  also; have "... = f 00 - f 00"; 
     by (rule linearform_diff) (simp!)+;
   also; have "... = 0r"; by simp;
-  finally; show "f <0> = 0r"; .;
+  finally; show "f 00 = 0r"; .;
 qed; 
 
 end;
\ No newline at end of file
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -19,12 +19,12 @@
   is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool"
   "is_seminorm V norm == ALL x: V. ALL y:V. ALL a. 
         0r <= norm x 
-      & norm (a <*> x) = (rabs a) * (norm x)
+      & norm (a (*) x) = (rabs a) * (norm x)
       & norm (x + y) <= norm x + norm y";
 
 lemma is_seminormI [intro]: 
   "[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x;
-  !! x a. x:V ==> norm (a <*> x) = (rabs a) * (norm x);
+  !! x a. x:V ==> norm (a (*) x) = (rabs a) * (norm x);
   !! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] 
   ==> is_seminorm V norm";
   by (unfold is_seminorm_def, force);
@@ -35,7 +35,7 @@
 
 lemma seminorm_rabs_homogenous: 
   "[| is_seminorm V norm; x:V |] 
-  ==> norm (a <*> x) = (rabs a) * (norm x)";
+  ==> norm (a (*) x) = (rabs a) * (norm x)";
   by (unfold is_seminorm_def, force);
 
 lemma seminorm_subadditive: 
@@ -48,11 +48,11 @@
   ==> norm (x - y) <= norm x + norm y";
 proof -;
   assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V";
-  have "norm (x - y) = norm (x + - 1r <*> y)";  
+  have "norm (x - y) = norm (x + - 1r (*) y)";  
     by (simp! add: diff_eq2 negate_eq2);
-  also; have "... <= norm x + norm  (- 1r <*> y)"; 
+  also; have "... <= norm x + norm  (- 1r (*) y)"; 
     by (simp! add: seminorm_subadditive);
-  also; have "norm (- 1r <*> y) = rabs (- 1r) * norm y"; 
+  also; have "norm (- 1r (*) y) = rabs (- 1r) * norm y"; 
     by (rule seminorm_rabs_homogenous);
   also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
   finally; show "norm (x - y) <= norm x + norm y"; by simp;
@@ -63,7 +63,7 @@
   ==> norm (- x) = norm x";
 proof -;
   assume "is_seminorm V norm" "x:V" "is_vectorspace V";
-  have "norm (- x) = norm (- 1r <*> x)"; by (simp! only: negate_eq1);
+  have "norm (- x) = norm (- 1r (*) x)"; by (simp! only: negate_eq1);
   also; have "... = rabs (- 1r) * norm x"; 
     by (rule seminorm_rabs_homogenous);
   also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
@@ -79,10 +79,10 @@
 constdefs
   is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
   "is_norm V norm == ALL x: V.  is_seminorm V norm 
-      & (norm x = 0r) = (x = <0>)";
+      & (norm x = 0r) = (x = 00)";
 
 lemma is_normI [intro]: 
-  "ALL x: V.  is_seminorm V norm  & (norm x = 0r) = (x = <0>) 
+  "ALL x: V.  is_seminorm V norm  & (norm x = 0r) = (x = 00) 
   ==> is_norm V norm"; by (simp only: is_norm_def);
 
 lemma norm_is_seminorm [intro??]: 
@@ -90,7 +90,7 @@
   by (unfold is_norm_def, force);
 
 lemma norm_zero_iff: 
-  "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)";
+  "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = 00)";
   by (unfold is_norm_def, force);
 
 lemma norm_ge_zero [intro??]:
@@ -128,15 +128,15 @@
   by (unfold is_normed_vectorspace_def, rule, elim conjE);
 
 lemma normed_vs_norm_gt_zero [intro??]: 
-  "[| is_normed_vectorspace V norm; x:V; x ~= <0> |] ==> 0r < norm x";
+  "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> 0r < norm x";
 proof (unfold is_normed_vectorspace_def, elim conjE);
-  assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm";
+  assume "x : V" "x ~= 00" "is_vectorspace V" "is_norm V norm";
   have "0r <= norm x"; ..;
   also; have "0r ~= norm x";
   proof;
     presume "norm x = 0r";
-    also; have "?this = (x = <0>)"; by (rule norm_zero_iff);
-    finally; have "x = <0>"; .;
+    also; have "?this = (x = 00)"; by (rule norm_zero_iff);
+    finally; have "x = 00"; .;
     thus "False"; by contradiction;
   qed (rule sym);
   finally; show "0r < norm x"; .;
@@ -144,7 +144,7 @@
 
 lemma normed_vs_norm_rabs_homogenous [intro??]: 
   "[| is_normed_vectorspace V norm; x:V |] 
-  ==> norm (a <*> x) = (rabs a) * (norm x)";
+  ==> norm (a (*) x) = (rabs a) * (norm x)";
   by (rule seminorm_rabs_homogenous, rule norm_is_seminorm, 
       rule normed_vs_norm);
 
@@ -170,13 +170,13 @@
     proof;
       fix x y a; presume "x : E";
       show "0r <= norm x"; ..;
-      show "norm (a <*> x) = rabs a * norm x"; ..;
+      show "norm (a (*) x) = rabs a * norm x"; ..;
       presume "y : E";
       show "norm (x + y) <= norm x + norm y"; ..;
     qed (simp!)+;
 
     fix x; assume "x : F";
-    show "(norm x = 0r) = (x = <0>)"; 
+    show "(norm x = 0r) = (x = 00)"; 
     proof (rule norm_zero_iff);
       show "is_norm E norm"; ..;
     qed (simp!);
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -18,14 +18,14 @@
 constdefs 
   is_subspace ::  "['a::{minus, plus} set, 'a set] => bool"
   "is_subspace U V == U ~= {} & U <= V 
-     & (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
+     & (ALL x:U. ALL y:U. ALL a. x + y : U & a (*) x : U)";
 
 lemma subspaceI [intro]: 
-  "[| <0> : U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
-  ALL x:U. ALL a. a <*> x : U |]
+  "[| 00 : U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
+  ALL x:U. ALL a. a (*) x : U |]
   ==> is_subspace U V";
 proof (unfold is_subspace_def, intro conjI); 
-  assume "<0> : U"; thus "U ~= {}"; by fast;
+  assume "00 : U"; thus "U ~= {}"; by fast;
 qed (simp+);
 
 lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}";
@@ -43,7 +43,7 @@
   by (unfold is_subspace_def) simp;
 
 lemma subspace_mult_closed [simp, intro??]: 
-  "[| is_subspace U V; x:U |] ==> a <*> x : U";
+  "[| is_subspace U V; x:U |] ==> a (*) x : U";
   by (unfold is_subspace_def) simp;
 
 lemma subspace_diff_closed [simp, intro??]: 
@@ -56,7 +56,7 @@
 of the carrier set and by vector space laws.*};
 
 lemma zero_in_subspace [intro??]:
-  "[| is_subspace U V; is_vectorspace V |] ==> <0> : U";
+  "[| is_subspace U V; is_vectorspace V |] ==> 00 : U";
 proof -; 
   assume "is_subspace U V" and v: "is_vectorspace V";
   have "U ~= {}"; ..;
@@ -65,7 +65,7 @@
   proof; 
     fix x; assume u: "x:U"; 
     hence "x:V"; by (simp!);
-    with v; have "<0> = x - x"; by (simp!);
+    with v; have "00 = x - x"; by (simp!);
     also; have "... : U"; by (rule subspace_diff_closed);
     finally; show ?thesis; .;
   qed;
@@ -84,10 +84,10 @@
   assume "is_subspace U V" "is_vectorspace V";
   show ?thesis;
   proof; 
-    show "<0> : U"; ..;
-    show "ALL x:U. ALL a. a <*> x : U"; by (simp!);
+    show "00 : U"; ..;
+    show "ALL x:U. ALL a. a (*) x : U"; by (simp!);
     show "ALL x:U. ALL y:U. x + y : U"; by (simp!);
-    show "ALL x:U. - x = -1r <*> x"; by (simp! add: negate_eq1);
+    show "ALL x:U. - x = -1r (*) x"; by (simp! add: negate_eq1);
     show "ALL x:U. ALL y:U. x - y =  x + - y"; 
       by (simp! add: diff_eq1);
   qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
@@ -98,10 +98,10 @@
 lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V";
 proof; 
   assume "is_vectorspace V";
-  show "<0> : V"; ..;
+  show "00 : V"; ..;
   show "V <= V"; ..;
   show "ALL x:V. ALL y:V. x + y : V"; by (simp!);
-  show "ALL x:V. ALL a. a <*> x : V"; by (simp!);
+  show "ALL x:V. ALL a. a (*) x : V"; by (simp!);
 qed;
 
 text {* The subspace relation is transitive. *};
@@ -111,7 +111,7 @@
   ==> is_subspace U W";
 proof; 
   assume "is_subspace U V" "is_subspace V W" "is_vectorspace V";
-  show "<0> : U"; ..;
+  show "00 : U"; ..;
 
   have "U <= V"; ..;
   also; have "V <= W"; ..;
@@ -123,10 +123,10 @@
     show "x + y : U"; by (simp!);
   qed;
 
-  show "ALL x:U. ALL a. a <*> x : U";
+  show "ALL x:U. ALL a. a (*) x : U";
   proof (intro ballI allI);
     fix x a; assume "x:U";
-    show "a <*> x : U"; by (simp!);
+    show "a (*) x : U"; by (simp!);
   qed;
 qed;
 
@@ -139,12 +139,12 @@
 
 constdefs
   lin :: "'a => 'a set"
-  "lin x == {a <*> x | a. True}"; 
+  "lin x == {a (*) x | a. True}"; 
 
-lemma linD: "x : lin v = (EX a::real. x = a <*> v)";
+lemma linD: "x : lin v = (EX a::real. x = a (*) v)";
   by (unfold lin_def) fast;
 
-lemma linI [intro??]: "a <*> x0 : lin x0";
+lemma linI [intro??]: "a (*) x0 : lin x0";
   by (unfold lin_def) fast;
 
 text {* Every vector is contained in its linear closure. *};
@@ -152,7 +152,7 @@
 lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x";
 proof (unfold lin_def, intro CollectI exI conjI);
   assume "is_vectorspace V" "x:V";
-  show "x = 1r <*> x"; by (simp!);
+  show "x = 1r (*) x"; by (simp!);
 qed simp;
 
 text {* Any linear closure is a subspace. *};
@@ -161,14 +161,14 @@
   "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
 proof;
   assume "is_vectorspace V" "x:V";
-  show "<0> : lin x"; 
+  show "00 : lin x"; 
   proof (unfold lin_def, intro CollectI exI conjI);
-    show "<0> = 0r <*> x"; by (simp!);
+    show "00 = 0r (*) x"; by (simp!);
   qed simp;
 
   show "lin x <= V";
   proof (unfold lin_def, intro subsetI, elim CollectE exE conjE); 
-    fix xa a; assume "xa = a <*> x"; 
+    fix xa a; assume "xa = a (*) x"; 
     show "xa:V"; by (simp!);
   qed;
 
@@ -178,20 +178,20 @@
     thus "x1 + x2 : lin x";
     proof (unfold lin_def, elim CollectE exE conjE, 
       intro CollectI exI conjI);
-      fix a1 a2; assume "x1 = a1 <*> x" "x2 = a2 <*> x";
-      show "x1 + x2 = (a1 + a2) <*> x"; 
+      fix a1 a2; assume "x1 = a1 (*) x" "x2 = a2 (*) x";
+      show "x1 + x2 = (a1 + a2) (*) x"; 
         by (simp! add: vs_add_mult_distrib2);
     qed simp;
   qed;
 
-  show "ALL xa:lin x. ALL a. a <*> xa : lin x"; 
+  show "ALL xa:lin x. ALL a. a (*) xa : lin x"; 
   proof (intro ballI allI);
     fix x1 a; assume "x1 : lin x"; 
-    thus "a <*> x1 : lin x";
+    thus "a (*) x1 : lin x";
     proof (unfold lin_def, elim CollectE exE conjE,
       intro CollectI exI conjI);
-      fix a1; assume "x1 = a1 <*> x";
-      show "a <*> x1 = (a * a1) <*> x"; by (simp!);
+      fix a1; assume "x1 = a1 (*) x";
+      show "a (*) x1 = (a * a1) (*) x"; by (simp!);
     qed simp;
   qed; 
 qed;
@@ -240,20 +240,20 @@
   ==> is_subspace U (U + V)";
 proof; 
   assume "is_vectorspace U" "is_vectorspace V";
-  show "<0> : U"; ..;
+  show "00 : U"; ..;
   show "U <= U + V";
   proof (intro subsetI vs_sumI);
   fix x; assume "x:U";
-    show "x = x + <0>"; by (simp!);
-    show "<0> : V"; by (simp!);
+    show "x = x + 00"; by (simp!);
+    show "00 : V"; by (simp!);
   qed;
   show "ALL x:U. ALL y:U. x + y : U"; 
   proof (intro ballI);
     fix x y; assume "x:U" "y:U"; show "x + y : U"; by (simp!);
   qed;
-  show "ALL x:U. ALL a. a <*> x : U"; 
+  show "ALL x:U. ALL a. a (*) x : U"; 
   proof (intro ballI allI);
-    fix x a; assume "x:U"; show "a <*> x : U"; by (simp!);
+    fix x a; assume "x:U"; show "a (*) x : U"; by (simp!);
   qed;
 qed;
 
@@ -264,11 +264,11 @@
   ==> is_subspace (U + V) E";
 proof; 
   assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
-  show "<0> : U + V";
+  show "00 : U + V";
   proof (intro vs_sumI);
-    show "<0> : U"; ..;
-    show "<0> : V"; ..;
-    show "(<0>::'a) = <0> + <0>"; by (simp!);
+    show "00 : U"; ..;
+    show "00 : V"; ..;
+    show "(00::'a) = 00 + 00"; by (simp!);
   qed;
   
   show "U + V <= E";
@@ -289,13 +289,13 @@
     qed (simp!)+;
   qed;
 
-  show "ALL x : U + V. ALL a. a <*> x : U + V";
+  show "ALL x : U + V. ALL a. a (*) x : U + V";
   proof (intro ballI allI);
     fix x a; assume "x : U + V";
-    thus "a <*> x : U + V";
+    thus "a (*) x : U + V";
     proof (elim vs_sumE bexE, intro vs_sumI);
       fix a x u v; assume "u : U" "v : V" "x = u + v";
-      show "a <*> x = (a <*> u) + (a <*> v)"; 
+      show "a (*) x = (a (*) u) + (a (*) v)"; 
         by (simp! add: vs_add_mult_distrib1);
     qed (simp!)+;
   qed;
@@ -323,11 +323,11 @@
 
 lemma decomp: 
   "[| is_vectorspace E; is_subspace U E; is_subspace V E; 
-  U Int V = {<0>}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |] 
+  U Int V = {00}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |] 
   ==> u1 = u2 & v1 = v2"; 
 proof; 
   assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"  
-    "U Int V = {<0>}" "u1:U" "u2:U" "v1:V" "v2:V" 
+    "U Int V = {00}" "u1:U" "u2:U" "v1:V" "v2:V" 
     "u1 + v1 = u2 + v2"; 
   have eq: "u1 - u2 = v2 - v1"; by (simp! add: vs_add_diff_swap);
   have u: "u1 - u2 : U"; by (simp!); 
@@ -337,14 +337,14 @@
   
   show "u1 = u2";
   proof (rule vs_add_minus_eq);
-    show "u1 - u2 = <0>"; by (rule Int_singletonD [OF _ u u']); 
+    show "u1 - u2 = 00"; by (rule Int_singletonD [OF _ u u']); 
     show "u1 : E"; ..;
     show "u2 : E"; ..;
   qed;
 
   show "v1 = v2";
   proof (rule vs_add_minus_eq [RS sym]);
-    show "v2 - v1 = <0>"; by (rule Int_singletonD [OF _ v' v]);
+    show "v2 - v1 = 00"; by (rule Int_singletonD [OF _ v' v]);
     show "v1 : E"; ..;
     show "v2 : E"; ..;
   qed;
@@ -358,44 +358,44 @@
 
 lemma decomp_H0: 
   "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 
-  x0 ~: H; x0 : E; x0 ~= <0>; y1 + a1 <*> x0 = y2 + a2 <*> x0 |]
+  x0 ~: H; x0 : E; x0 ~= 00; y1 + a1 (*) x0 = y2 + a2 (*) x0 |]
   ==> y1 = y2 & a1 = a2";
 proof;
   assume "is_vectorspace E" and h: "is_subspace H E"
-     and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
-         "y1 + a1 <*> x0 = y2 + a2 <*> x0";
+     and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= 00" 
+         "y1 + a1 (*) x0 = y2 + a2 (*) x0";
 
-  have c: "y1 = y2 & a1 <*> x0 = a2 <*> x0";
+  have c: "y1 = y2 & a1 (*) x0 = a2 (*) x0";
   proof (rule decomp); 
-    show "a1 <*> x0 : lin x0"; ..; 
-    show "a2 <*> x0 : lin x0"; ..;
-    show "H Int (lin x0) = {<0>}"; 
+    show "a1 (*) x0 : lin x0"; ..; 
+    show "a2 (*) x0 : lin x0"; ..;
+    show "H Int (lin x0) = {00}"; 
     proof;
-      show "H Int lin x0 <= {<0>}"; 
+      show "H Int lin x0 <= {00}"; 
       proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
         fix x; assume "x:H" "x : lin x0"; 
-        thus "x = <0>";
+        thus "x = 00";
         proof (unfold lin_def, elim CollectE exE conjE);
-          fix a; assume "x = a <*> x0";
+          fix a; assume "x = a (*) x0";
           show ?thesis;
           proof cases;
             assume "a = 0r"; show ?thesis; by (simp!);
           next;
             assume "a ~= 0r"; 
-            from h; have "rinv a <*> a <*> x0 : H"; 
+            from h; have "rinv a (*) a (*) x0 : H"; 
               by (rule subspace_mult_closed) (simp!);
-            also; have "rinv a <*> a <*> x0 = x0"; by (simp!);
+            also; have "rinv a (*) a (*) x0 = x0"; by (simp!);
             finally; have "x0 : H"; .;
             thus ?thesis; by contradiction;
           qed;
        qed;
       qed;
-      show "{<0>} <= H Int lin x0";
+      show "{00} <= H Int lin x0";
       proof -;
-	have "<0>: H Int lin x0";
+	have "00: H Int lin x0";
 	proof (rule IntI);
-	  show "<0>:H"; ..;
-	  from lin_vs; show "<0> : lin x0"; ..;
+	  show "00:H"; ..;
+	  from lin_vs; show "00 : lin x0"; ..;
 	qed;
 	thus ?thesis; by simp;
       qed;
@@ -407,7 +407,7 @@
   
   show  "a1 = a2"; 
   proof (rule vs_mult_right_cancel [RS iffD1]);
-    from c; show "a1 <*> x0 = a2 <*> x0"; by simp;
+    from c; show "a1 (*) x0 = a2 (*) x0"; by simp;
   qed;
 qed;
 
@@ -418,13 +418,13 @@
 
 lemma decomp_H0_H: 
   "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
-  x0 ~= <0> |] 
-  ==> (SOME (y, a). t = y + a <*> x0 & y : H) = (t, 0r)";
+  x0 ~= 00 |] 
+  ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, 0r)";
 proof (rule, unfold split_paired_all);
   assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
-    "x0 ~= <0>";
+    "x0 ~= 00";
   have h: "is_vectorspace H"; ..;
-  fix y a; presume t1: "t = y + a <*> x0" and "y:H";
+  fix y a; presume t1: "t = y + a (*) x0" and "y:H";
   have "y = t & a = 0r"; 
     by (rule decomp_H0) (assumption | (simp!))+;
   thus "(y, a) = (t, 0r)"; by (simp!);
@@ -435,40 +435,40 @@
 $h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
 
 lemma h0_definite:
-  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
+  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H)
                 in (h y) + a * xi);
-  x = y + a <*> x0; is_vectorspace E; is_subspace H E;
-  y:H; x0 ~: H; x0:E; x0 ~= <0> |]
+  x = y + a (*) x0; is_vectorspace E; is_subspace H E;
+  y:H; x0 ~: H; x0:E; x0 ~= 00 |]
   ==> h0 x = h y + a * xi";
 proof -;  
   assume 
-    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
+    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H)
                in (h y) + a * xi)"
-    "x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
-    "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
+    "x = y + a (*) x0" "is_vectorspace E" "is_subspace H E"
+    "y:H" "x0 ~: H" "x0:E" "x0 ~= 00";
   have "x : H + (lin x0)"; 
     by (simp! add: vs_sum_def lin_def) force+;
-  have "EX! xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)"; 
+  have "EX! xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)"; 
   proof;
-    show "EX xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
+    show "EX xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)";
       by (force!);
   next;
     fix xa ya;
-    assume "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
-           "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
+    assume "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) xa"
+           "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) ya";
     show "xa = ya"; ;
     proof -;
       show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
         by (rule Pair_fst_snd_eq [RS iffD2]);
-      have x: "x = fst xa + snd xa <*> x0 & fst xa : H"; 
+      have x: "x = fst xa + snd xa (*) x0 & fst xa : H"; 
         by (force!);
-      have y: "x = fst ya + snd ya <*> x0 & fst ya : H"; 
+      have y: "x = fst ya + snd ya (*) x0 & fst ya : H"; 
         by (force!);
       from x y; show "fst xa = fst ya & snd xa = snd ya"; 
         by (elim conjE) (rule decomp_H0, (simp!)+);
     qed;
   qed;
-  hence eq: "(SOME (y, a). x = y + a <*> x0 & y:H) = (y, a)"; 
+  hence eq: "(SOME (y, a). x = y + a (*) x0 & y:H) = (y, a)"; 
     by (rule select1_equality) (force!);
   thus "h0 x = h y + a * xi"; by (simp! add: Let_def);
 qed;
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -15,8 +15,8 @@
 element $\zero$ is defined. *};
 
 consts
-  prod  :: "[real, 'a] => 'a"                       (infixr "<*>" 70)
-  zero  :: 'a                                       ("<0>");
+  prod  :: "[real, 'a] => 'a"                       (infixr "'(*')" 70)
+  zero  :: 'a                                       ("00");
 
 syntax (symbols)
   prod  :: "[real, 'a] => 'a"                       (infixr "\<prod>" 70)
@@ -29,7 +29,7 @@
 (***
 constdefs 
   negate :: "'a => 'a"                           ("- _" [100] 100)
-  "- x == (- 1r) <*> x"
+  "- x == (- 1r) ( * ) x"
   diff :: "'a => 'a => 'a"                       (infixl "-" 68)
   "x - y == x + - y";
 ***)
@@ -51,34 +51,34 @@
   "is_vectorspace V == V ~= {} 
    & (ALL x:V. ALL y:V. ALL z:V. ALL a b.
         x + y : V                                 
-      & a <*> x : V                                 
+      & a (*) x : V                                 
       & (x + y) + z = x + (y + z)             
       & x + y = y + x                           
-      & x - x = <0>                               
-      & <0> + x = x                               
-      & a <*> (x + y) = a <*> x + a <*> y       
-      & (a + b) <*> x = a <*> x + b <*> x         
-      & (a * b) <*> x = a <*> b <*> x               
-      & 1r <*> x = x
-      & - x = (- 1r) <*> x
+      & x - x = 00                               
+      & 00 + x = x                               
+      & a (*) (x + y) = a (*) x + a (*) y       
+      & (a + b) (*) x = a (*) x + b (*) x         
+      & (a * b) (*) x = a (*) b (*) x               
+      & 1r (*) x = x
+      & - x = (- 1r) (*) x
       & x - y = x + - y)";                             
 
 text_raw {* \medskip *};
 text {* The corresponding introduction rule is:*};
 
 lemma vsI [intro]:
-  "[| <0>:V; 
+  "[| 00:V; 
   ALL x:V. ALL y:V. x + y : V; 
-  ALL x:V. ALL a. a <*> x : V;  
+  ALL x:V. ALL a. a (*) x : V;  
   ALL x:V. ALL y:V. ALL z:V. (x + y) + z = x + (y + z);
   ALL x:V. ALL y:V. x + y = y + x;
-  ALL x:V. x - x = <0>;
-  ALL x:V. <0> + x = x;
-  ALL x:V. ALL y:V. ALL a. a <*> (x + y) = a <*> x + a <*> y;
-  ALL x:V. ALL a b. (a + b) <*> x = a <*> x + b <*> x;
-  ALL x:V. ALL a b. (a * b) <*> x = a <*> b <*> x; 
-  ALL x:V. 1r <*> x = x; 
-  ALL x:V. - x = (- 1r) <*> x; 
+  ALL x:V. x - x = 00;
+  ALL x:V. 00 + x = x;
+  ALL x:V. ALL y:V. ALL a. a (*) (x + y) = a (*) x + a (*) y;
+  ALL x:V. ALL a b. (a + b) (*) x = a (*) x + b (*) x;
+  ALL x:V. ALL a b. (a * b) (*) x = a (*) b (*) x; 
+  ALL x:V. 1r (*) x = x; 
+  ALL x:V. - x = (- 1r) (*) x; 
   ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V";
 proof (unfold is_vectorspace_def, intro conjI ballI allI);
   fix x y z; 
@@ -91,7 +91,7 @@
 text {* The corresponding destruction rules are: *};
 
 lemma negate_eq1: 
-  "[| is_vectorspace V; x:V |] ==> - x = (- 1r) <*> x";
+  "[| is_vectorspace V; x:V |] ==> - x = (- 1r) (*) x";
   by (unfold is_vectorspace_def) simp;
 
 lemma diff_eq1: 
@@ -99,7 +99,7 @@
   by (unfold is_vectorspace_def) simp; 
 
 lemma negate_eq2: 
-  "[| is_vectorspace V; x:V |] ==> (- 1r) <*> x = - x";
+  "[| is_vectorspace V; x:V |] ==> (- 1r) (*) x = - x";
   by (unfold is_vectorspace_def) simp;
 
 lemma diff_eq2: 
@@ -114,7 +114,7 @@
   by (unfold is_vectorspace_def) simp;
 
 lemma vs_mult_closed [simp, intro??]: 
-  "[| is_vectorspace V; x:V |] ==> a <*> x : V"; 
+  "[| is_vectorspace V; x:V |] ==> a (*) x : V"; 
   by (unfold is_vectorspace_def) simp;
 
 lemma vs_diff_closed [simp, intro??]: 
@@ -149,13 +149,13 @@
 theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute;
 
 lemma vs_diff_self [simp]: 
-  "[| is_vectorspace V; x:V |] ==>  x - x = <0>"; 
+  "[| is_vectorspace V; x:V |] ==>  x - x = 00"; 
   by (unfold is_vectorspace_def) simp;
 
 text {* The existence of the zero element of a vector space
 follows from the non-emptiness of carrier set. *};
 
-lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
+lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 00:V";
 proof -; 
   assume "is_vectorspace V";
   have "V ~= {}"; ..;
@@ -163,64 +163,64 @@
   thus ?thesis; 
   proof; 
     fix x; assume "x:V"; 
-    have "<0> = x - x"; by (simp!);
+    have "00 = x - x"; by (simp!);
     also; have "... : V"; by (simp! only: vs_diff_closed);
     finally; show ?thesis; .;
   qed;
 qed;
 
 lemma vs_add_zero_left [simp]: 
-  "[| is_vectorspace V; x:V |] ==>  <0> + x = x";
+  "[| is_vectorspace V; x:V |] ==>  00 + x = x";
   by (unfold is_vectorspace_def) simp;
 
 lemma vs_add_zero_right [simp]: 
-  "[| is_vectorspace V; x:V |] ==>  x + <0> = x";
+  "[| is_vectorspace V; x:V |] ==>  x + 00 = x";
 proof -;
   assume "is_vectorspace V" "x:V";
-  hence "x + <0> = <0> + x"; by simp;
+  hence "x + 00 = 00 + x"; by simp;
   also; have "... = x"; by (simp!);
   finally; show ?thesis; .;
 qed;
 
 lemma vs_add_mult_distrib1: 
   "[| is_vectorspace V; x:V; y:V |] 
-  ==> a <*> (x + y) = a <*> x + a <*> y";
+  ==> a (*) (x + y) = a (*) x + a (*) y";
   by (unfold is_vectorspace_def) simp;
 
 lemma vs_add_mult_distrib2: 
   "[| is_vectorspace V; x:V |] 
-  ==> (a + b) <*> x = a <*> x + b <*> x"; 
+  ==> (a + b) (*) x = a (*) x + b (*) x"; 
   by (unfold is_vectorspace_def) simp;
 
 lemma vs_mult_assoc: 
-  "[| is_vectorspace V; x:V |] ==> (a * b) <*> x = a <*> (b <*> x)";
+  "[| is_vectorspace V; x:V |] ==> (a * b) (*) x = a (*) (b (*) x)";
   by (unfold is_vectorspace_def) simp;
 
 lemma vs_mult_assoc2 [simp]: 
- "[| is_vectorspace V; x:V |] ==> a <*> b <*> x = (a * b) <*> x";
+ "[| is_vectorspace V; x:V |] ==> a (*) b (*) x = (a * b) (*) x";
   by (simp only: vs_mult_assoc);
 
 lemma vs_mult_1 [simp]: 
-  "[| is_vectorspace V; x:V |] ==> 1r <*> x = x"; 
+  "[| is_vectorspace V; x:V |] ==> 1r (*) x = x"; 
   by (unfold is_vectorspace_def) simp;
 
 lemma vs_diff_mult_distrib1: 
   "[| is_vectorspace V; x:V; y:V |] 
-  ==> a <*> (x - y) = a <*> x - a <*> y";
+  ==> a (*) (x - y) = a (*) x - a (*) y";
   by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1);
 
 lemma vs_diff_mult_distrib2: 
   "[| is_vectorspace V; x:V |] 
-  ==> (a - b) <*> x = a <*> x - (b <*> x)";
+  ==> (a - b) (*) x = a (*) x - (b (*) x)";
 proof -;
   assume "is_vectorspace V" "x:V";
-  have " (a - b) <*> x = (a + - b ) <*> x"; 
+  have " (a - b) (*) x = (a + - b ) (*) x"; 
     by (unfold real_diff_def, simp);
-  also; have "... = a <*> x + (- b) <*> x"; 
+  also; have "... = a (*) x + (- b) (*) x"; 
     by (rule vs_add_mult_distrib2);
-  also; have "... = a <*> x + - (b <*> x)"; 
+  also; have "... = a (*) x + - (b (*) x)"; 
     by (simp! add: negate_eq1);
-  also; have "... = a <*> x - (b <*> x)"; 
+  also; have "... = a (*) x - (b (*) x)"; 
     by (simp! add: diff_eq1);
   finally; show ?thesis; .;
 qed;
@@ -230,34 +230,34 @@
 text{* Further derived laws: *};
 
 lemma vs_mult_zero_left [simp]: 
-  "[| is_vectorspace V; x:V |] ==> 0r <*> x = <0>";
+  "[| is_vectorspace V; x:V |] ==> 0r (*) x = 00";
 proof -;
   assume "is_vectorspace V" "x:V";
-  have  "0r <*> x = (1r - 1r) <*> x"; by (simp only: real_diff_self);
-  also; have "... = (1r + - 1r) <*> x"; by simp;
-  also; have "... =  1r <*> x + (- 1r) <*> x"; 
+  have  "0r (*) x = (1r - 1r) (*) x"; by (simp only: real_diff_self);
+  also; have "... = (1r + - 1r) (*) x"; by simp;
+  also; have "... =  1r (*) x + (- 1r) (*) x"; 
     by (rule vs_add_mult_distrib2);
-  also; have "... = x + (- 1r) <*> x"; by (simp!);
+  also; have "... = x + (- 1r) (*) x"; by (simp!);
   also; have "... = x + - x"; by (simp! add: negate_eq2);;
   also; have "... = x - x"; by (simp! add: diff_eq2);
-  also; have "... = <0>"; by (simp!);
+  also; have "... = 00"; by (simp!);
   finally; show ?thesis; .;
 qed;
 
 lemma vs_mult_zero_right [simp]: 
   "[| is_vectorspace (V:: 'a::{plus, minus} set) |] 
-  ==> a <*> <0> = (<0>::'a)";
+  ==> a (*) 00 = (00::'a)";
 proof -;
   assume "is_vectorspace V";
-  have "a <*> <0> = a <*> (<0> - (<0>::'a))"; by (simp!);
-  also; have "... =  a <*> <0> - a <*> <0>";
+  have "a (*) 00 = a (*) (00 - (00::'a))"; by (simp!);
+  also; have "... =  a (*) 00 - a (*) 00";
      by (rule vs_diff_mult_distrib1) (simp!)+;
-  also; have "... = <0>"; by (simp!);
+  also; have "... = 00"; by (simp!);
   finally; show ?thesis; .;
 qed;
 
 lemma vs_minus_mult_cancel [simp]:  
-  "[| is_vectorspace V; x:V |] ==> (- a) <*> - x = a <*> x";
+  "[| is_vectorspace V; x:V |] ==> (- a) (*) - x = a (*) x";
   by (simp add: negate_eq1);
 
 lemma vs_add_minus_left_eq_diff: 
@@ -271,11 +271,11 @@
 qed;
 
 lemma vs_add_minus [simp]: 
-  "[| is_vectorspace V; x:V |] ==> x + - x = <0>";
+  "[| is_vectorspace V; x:V |] ==> x + - x = 00";
   by (simp! add: diff_eq2);
 
 lemma vs_add_minus_left [simp]: 
-  "[| is_vectorspace V; x:V |] ==> - x + x = <0>";
+  "[| is_vectorspace V; x:V |] ==> - x + x = 00";
   by (simp! add: diff_eq2);
 
 lemma vs_minus_minus [simp]: 
@@ -283,11 +283,11 @@
   by (simp add: negate_eq1);
 
 lemma vs_minus_zero [simp]: 
-  "is_vectorspace (V::'a::{minus, plus} set) ==> - (<0>::'a) = <0>"; 
+  "is_vectorspace (V::'a::{minus, plus} set) ==> - (00::'a) = 00"; 
   by (simp add: negate_eq1);
 
 lemma vs_minus_zero_iff [simp]:
-  "[| is_vectorspace V; x:V |] ==> (- x = <0>) = (x = <0>)" 
+  "[| is_vectorspace V; x:V |] ==> (- x = 00) = (x = 00)" 
   (concl is "?L = ?R");
 proof -;
   assume "is_vectorspace V" "x:V";
@@ -295,7 +295,7 @@
   proof;
     have "x = - (- x)"; by (rule vs_minus_minus [RS sym]);
     also; assume ?L;
-    also; have "- ... = <0>"; by (rule vs_minus_zero);
+    also; have "- ... = 00"; by (rule vs_minus_zero);
     finally; show ?R; .;
   qed (simp!);
 qed;
@@ -314,11 +314,11 @@
   by (simp add: negate_eq1 vs_add_mult_distrib1);
 
 lemma vs_diff_zero [simp]: 
-  "[| is_vectorspace V; x:V |] ==> x - <0> = x";
+  "[| is_vectorspace V; x:V |] ==> x - 00 = x";
   by (simp add: diff_eq1);  
 
 lemma vs_diff_zero_right [simp]: 
-  "[| is_vectorspace V; x:V |] ==> <0> - x = - x";
+  "[| is_vectorspace V; x:V |] ==> 00 - x = - x";
   by (simp add:diff_eq1);
 
 lemma vs_add_left_cancel:
@@ -327,7 +327,7 @@
   (concl is "?L = ?R");
 proof;
   assume "is_vectorspace V" "x:V" "y:V" "z:V";
-  have "y = <0> + y"; by (simp!);
+  have "y = 00 + y"; by (simp!);
   also; have "... = - x + x + y"; by (simp!);
   also; have "... = - x + (x + y)"; 
     by (simp! only: vs_add_assoc vs_neg_closed);
@@ -350,66 +350,66 @@
 
 lemma vs_mult_left_commute: 
   "[| is_vectorspace V; x:V; y:V; z:V |] 
-  ==> x <*> y <*> z = y <*> x <*> z";  
+  ==> x (*) y (*) z = y (*) x (*) z";  
   by (simp add: real_mult_commute);
 
 lemma vs_mult_zero_uniq :
-  "[| is_vectorspace V; x:V; a <*> x = <0>; x ~= <0> |] ==> a = 0r";
+  "[| is_vectorspace V; x:V; a (*) x = 00; x ~= 00 |] ==> a = 0r";
 proof (rule classical);
-  assume "is_vectorspace V" "x:V" "a <*> x = <0>" "x ~= <0>";
+  assume "is_vectorspace V" "x:V" "a (*) x = 00" "x ~= 00";
   assume "a ~= 0r";
-  have "x = (rinv a * a) <*> x"; by (simp!);
-  also; have "... = rinv a <*> (a <*> x)"; by (rule vs_mult_assoc);
-  also; have "... = rinv a <*> <0>"; by (simp!);
-  also; have "... = <0>"; by (simp!);
-  finally; have "x = <0>"; .;
+  have "x = (rinv a * a) (*) x"; by (simp!);
+  also; have "... = rinv a (*) (a (*) x)"; by (rule vs_mult_assoc);
+  also; have "... = rinv a (*) 00"; by (simp!);
+  also; have "... = 00"; by (simp!);
+  finally; have "x = 00"; .;
   thus "a = 0r"; by contradiction; 
 qed;
 
 lemma vs_mult_left_cancel: 
   "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==> 
-  (a <*> x = a <*> y) = (x = y)"
+  (a (*) x = a (*) y) = (x = y)"
   (concl is "?L = ?R");
 proof;
   assume "is_vectorspace V" "x:V" "y:V" "a ~= 0r";
-  have "x = 1r <*> x"; by (simp!);
-  also; have "... = (rinv a * a) <*> x"; by (simp!);
-  also; have "... = rinv a <*> (a <*> x)"; 
+  have "x = 1r (*) x"; by (simp!);
+  also; have "... = (rinv a * a) (*) x"; by (simp!);
+  also; have "... = rinv a (*) (a (*) x)"; 
     by (simp! only: vs_mult_assoc);
   also; assume ?L;
-  also; have "rinv a <*> ... = y"; by (simp!);
+  also; have "rinv a (*) ... = y"; by (simp!);
   finally; show ?R; .;
 qed simp;
 
 lemma vs_mult_right_cancel: (*** forward ***)
-  "[| is_vectorspace V; x:V; x ~= <0> |] 
-  ==> (a <*> x = b <*> x) = (a = b)" (concl is "?L = ?R");
+  "[| is_vectorspace V; x:V; x ~= 00 |] 
+  ==> (a (*) x = b (*) x) = (a = b)" (concl is "?L = ?R");
 proof;
-  assume "is_vectorspace V" "x:V" "x ~= <0>";
-  have "(a - b) <*> x = a <*> x - b <*> x"; 
+  assume "is_vectorspace V" "x:V" "x ~= 00";
+  have "(a - b) (*) x = a (*) x - b (*) x"; 
     by (simp! add: vs_diff_mult_distrib2);
-  also; assume ?L; hence "a <*> x - b <*> x = <0>"; by (simp!);
-  finally; have "(a - b) <*> x = <0>"; .; 
+  also; assume ?L; hence "a (*) x - b (*) x = 00"; by (simp!);
+  finally; have "(a - b) (*) x = 00"; .; 
   hence "a - b = 0r"; by (simp! add: vs_mult_zero_uniq);
   thus "a = b"; by (rule real_add_minus_eq);
 qed simp; (*** 
 
 backward :
 lemma vs_mult_right_cancel: 
-  "[| is_vectorspace V; x:V; x ~= <0> |] ==>  
-  (a <*> x = b <*> x) = (a = b)"
+  "[| is_vectorspace V; x:V; x ~= 00 |] ==>  
+  (a ( * ) x = b ( * ) x) = (a = b)"
   (concl is "?L = ?R");
 proof;
-  assume "is_vectorspace V" "x:V" "x ~= <0>";
+  assume "is_vectorspace V" "x:V" "x ~= 00";
   assume l: ?L; 
   show "a = b"; 
   proof (rule real_add_minus_eq);
     show "a - b = 0r"; 
     proof (rule vs_mult_zero_uniq);
-      have "(a - b) <*> x = a <*> x - b <*> x";
+      have "(a - b) ( * ) x = a ( * ) x - b ( * ) x";
         by (simp! add: vs_diff_mult_distrib2);
-      also; from l; have "a <*> x - b <*> x = <0>"; by (simp!);
-      finally; show "(a - b) <*> x  = <0>"; .; 
+      also; from l; have "a ( * ) x - b ( * ) x = 00"; by (simp!);
+      finally; show "(a - b) ( * ) x  = 00"; .; 
     qed;
   qed;
 next;
@@ -431,7 +431,7 @@
     also; have "... = z + - y + y"; by (simp! add: diff_eq1);
     also; have "... = z + (- y + y)"; 
       by (rule vs_add_assoc) (simp!)+;
-    also; from vs; have "... = z + <0>"; 
+    also; from vs; have "... = z + 00"; 
       by (simp only: vs_add_minus_left);
     also; from vs; have "... = z"; by (simp only: vs_add_zero_right);
     finally; show ?R; .;
@@ -448,22 +448,22 @@
 qed;
 
 lemma vs_add_minus_eq_minus: 
-  "[| is_vectorspace V; x:V; y:V; x + y = <0> |] ==> x = - y"; 
+  "[| is_vectorspace V; x:V; y:V; x + y = 00 |] ==> x = - y"; 
 proof -;
   assume "is_vectorspace V" "x:V" "y:V"; 
   have "x = (- y + y) + x"; by (simp!);
   also; have "... = - y + (x + y)"; by (simp!);
-  also; assume "x + y = <0>";
-  also; have "- y + <0> = - y"; by (simp!);
+  also; assume "x + y = 00";
+  also; have "- y + 00 = - y"; by (simp!);
   finally; show "x = - y"; .;
 qed;
 
 lemma vs_add_minus_eq: 
-  "[| is_vectorspace V; x:V; y:V; x - y = <0> |] ==> x = y"; 
+  "[| is_vectorspace V; x:V; y:V; x - y = 00 |] ==> x = y"; 
 proof -;
-  assume "is_vectorspace V" "x:V" "y:V" "x - y = <0>";
-  assume "x - y = <0>";
-  hence e: "x + - y = <0>"; by (simp! add: diff_eq1);
+  assume "is_vectorspace V" "x:V" "y:V" "x - y = 00";
+  assume "x - y = 00";
+  hence e: "x + - y = 00"; by (simp! add: diff_eq1);
   with _ _ _; have "x = - (- y)"; 
     by (rule vs_add_minus_eq_minus) (simp!)+;
   thus "x = y"; by (simp!);
@@ -514,12 +514,12 @@
   show "?L = ?R";
   proof;
     assume l: ?L;
-    have "x + z = <0>"; 
+    have "x + z = 00"; 
     proof (rule vs_add_left_cancel [RS iffD1]);
       have "y + (x + z) = x + (y + z)"; by (simp!);
       also; note l;
-      also; have "y = y + <0>"; by (simp!);
-      finally; show "y + (x + z) = y + <0>"; .;
+      also; have "y = y + 00"; by (simp!);
+      finally; show "y + (x + z) = y + 00"; .;
     qed (simp!)+;
     thus "x = - z"; by (simp! add: vs_add_minus_eq_minus);
   next;
@@ -532,4 +532,4 @@
   qed;
 qed;
 
-end;
\ No newline at end of file
+end;
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Relation.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -63,7 +63,7 @@
 by (Blast_tac 1);
 qed "diag_iff";
 
-Goal "diag(A) <= A Times A";
+Goal "diag(A) <= A <*> A";
 by (Blast_tac 1);
 qed "diag_subset_Times";
 
@@ -115,14 +115,14 @@
 by (Blast_tac 1);
 qed "comp_mono";
 
-Goal "[| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
+Goal "[| s <= A <*> B;  r <= B <*> C |] ==> (r O s) <= A <*> C";
 by (Blast_tac 1);
 qed "comp_subset_Sigma";
 
 (** Natural deduction for refl(r) **)
 
 val prems = Goalw [refl_def]
-    "[| r <= A Times A;  !! x. x:A ==> (x,x):r |] ==> refl A r";
+    "[| r <= A <*> A;  !! x. x:A ==> (x,x):r |] ==> refl A r";
 by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
 qed "reflI";
 
@@ -371,7 +371,7 @@
 by (Blast_tac 1);
 qed "Image_Un";
 
-Goal "r <= A Times B ==> r^^C <= B";
+Goal "r <= A <*> B ==> r^^C <= B";
 by (rtac subsetI 1);
 by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
 qed "Image_subset";
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Relation.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -29,7 +29,7 @@
     "Range(r) == Domain(r^-1)"
 
   refl   :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
-    "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)"
+    "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)"
 
   sym    :: "('a*'a) set=>bool"             (*symmetry predicate*)
     "sym(r) == ALL x y. (x,y): r --> (y,x): r"
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Sexp.ML
--- a/src/HOL/Sexp.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Sexp.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -49,7 +49,7 @@
 
 (** Introduction rules for 'pred_sexp' **)
 
-Goalw [pred_sexp_def] "pred_sexp <= sexp Times sexp";
+Goalw [pred_sexp_def] "pred_sexp <= sexp <*> sexp";
 by (Blast_tac 1);
 qed "pred_sexp_subset_Sigma";
 
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Subst/Unify.thy
--- a/src/HOL/Subst/Unify.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Subst/Unify.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -19,7 +19,7 @@
     --either the set of variables decreases
     --or the first argument does (in fact, both do)
   *)
-  unifyRel_def  "unifyRel == inv_image  (finite_psubset ** measure uterm_size)
+  unifyRel_def  "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size)
                                (%(M,N). (vars_of M Un vars_of N, M))"
 
 recdef unify "unifyRel"
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Trancl.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -342,12 +342,12 @@
 by (auto_tac (claset() addIs [r_into_trancl], simpset()));
 qed "irrefl_tranclI";
 
-Goal "[| (a,b) : r^*;  r <= A Times A |] ==> a=b | a:A";
+Goal "[| (a,b) : r^*;  r <= A <*> A |] ==> a=b | a:A";
 by (etac rtrancl_induct 1);
 by Auto_tac;
 val lemma = result();
 
-Goalw [trancl_def] "r <= A Times A ==> r^+ <= A Times A";
+Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
 by (blast_tac (claset() addSDs [lemma]) 1);
 qed "trancl_subset_Sigma";
 
diff -r 78b7010db847 -r 816d8f6513be src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/Extend.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -17,7 +17,7 @@
      (*Using the locale constant "f", this is  f (h (x,y))) = x*)
   
   extend_set :: "['a*'b => 'c, 'a set] => 'c set"
-    "extend_set h A == h `` (A Times UNIV)"
+    "extend_set h A == h `` (A <*> UNIV)"
 
   project_set :: "['a*'b => 'c, 'c set] => 'a set"
     "project_set h C == {x. EX y. h(x,y) : C}"
diff -r 78b7010db847 -r 816d8f6513be src/HOL/UNITY/LessThan.thy
--- a/src/HOL/UNITY/LessThan.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/LessThan.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -14,7 +14,7 @@
 
   (*MOVE TO RELATION.THY??*)
   Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
-    "Restrict A r == r Int (A Times UNIV)"
+    "Restrict A r == r Int (A <*> UNIV)"
 
   lessThan   :: "nat => nat set"
      "lessThan n == {i. i<n}"
diff -r 78b7010db847 -r 816d8f6513be src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -254,20 +254,20 @@
 by (Force_tac 1);
 qed "delete_map_neq_apply";
 
-(*A set of the form (A Times UNIV) ignores the second (dummy) state component*)
+(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
 
-Goal "(f o fst) -`` A = (f-``A) Times UNIV";
+Goal "(f o fst) -`` A = (f-``A) <*> UNIV";
 by Auto_tac;
 qed "vimage_o_fst_eq";
 
-Goal "(sub i -``A) Times UNIV = lift_set i (A Times UNIV)";
+Goal "(sub i -``A) <*> UNIV = lift_set i (A <*> UNIV)";
 by Auto_tac;
 qed "vimage_sub_eq_lift_set";
 
 Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set];
 
 Goal "[| F : preserves snd;  i~=j |] \
-\     ==> lift j F : stable (lift_set i (A Times UNIV))";
+\     ==> lift j F : stable (lift_set i (A <*> UNIV))";
 by (auto_tac (claset(),
 	      simpset() addsimps [lift_def, lift_set_def, 
 				  stable_def, constrains_def, 
@@ -280,9 +280,9 @@
 
 (*If i~=j then lift j F  does nothing to lift_set i, and the 
   premise ensures A<=B.*)
-Goal "[| F i : (A Times UNIV) co (B Times UNIV);  \
+Goal "[| F i : (A <*> UNIV) co (B <*> UNIV);  \
 \        F j : preserves snd |]  \
-\  ==> lift j (F j) : (lift_set i (A Times UNIV)) co (lift_set i (B Times UNIV))";
+\  ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))";
 by (case_tac "i=j" 1);
 by (asm_full_simp_tac (simpset() addsimps [lift_def, lift_set_def, 
 					   rename_constrains]) 1);
@@ -323,8 +323,8 @@
 qed "lift_map_eq_diff";
 
 Goal "F : preserves snd \
-\     ==> (lift i F : transient (lift_set j (A Times UNIV))) = \
-\         (i=j & F : transient (A Times UNIV) | A={})";
+\     ==> (lift i F : transient (lift_set j (A <*> UNIV))) = \
+\         (i=j & F : transient (A <*> UNIV) | A={})";
 by (case_tac "i=j" 1);
 by (auto_tac (claset(), simpset() addsimps [lift_transient]));
 by (auto_tac (claset(),
@@ -349,8 +349,8 @@
 qed "lift_transient_eq_disj";
 
 (*USELESS??*)
-Goal "lift_map i `` (A Times UNIV) = \
-\     (UN s:A. UN f. {insert_map i s f}) Times UNIV";
+Goal "lift_map i `` (A <*> UNIV) = \
+\     (UN s:A. UN f. {insert_map i s f}) <*> UNIV";
 by (auto_tac (claset() addSIs [bexI, image_eqI],
               simpset() addsimps [lift_map_def]));
 by (rtac (split RS sym) 1);
diff -r 78b7010db847 -r 816d8f6513be src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/PPROD.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -49,9 +49,9 @@
 (** Safety & Progress **)
 
 Goal "[| i : I;  ALL j. F j : preserves snd |] ==>  \
-\     (PLam I F : (lift_set i (A Times UNIV)) co \
-\                 (lift_set i (B Times UNIV)))  =  \
-\     (F i : (A Times UNIV) co (B Times UNIV))";
+\     (PLam I F : (lift_set i (A <*> UNIV)) co \
+\                 (lift_set i (B <*> UNIV)))  =  \
+\     (F i : (A <*> UNIV) co (B <*> UNIV))";
 by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains,
 				      Join_constrains]) 1);
 by (stac (insert_Diff RS sym) 1 THEN assume_tac 1);
@@ -60,8 +60,8 @@
 qed "PLam_constrains";
 
 Goal "[| i : I;  ALL j. F j : preserves snd |]  \
-\     ==> (PLam I F : stable (lift_set i (A Times UNIV))) = \
-\         (F i : stable (A Times UNIV))";
+\     ==> (PLam I F : stable (lift_set i (A <*> UNIV))) = \
+\         (F i : stable (A <*> UNIV))";
 by (asm_simp_tac (simpset() addsimps [stable_def, PLam_constrains]) 1);
 qed "PLam_stable";
 
@@ -73,9 +73,9 @@
 Addsimps [PLam_constrains, PLam_stable, PLam_transient];
 
 (*This holds because the F j cannot change (lift_set i)*)
-Goal "[| i : I;  F i : (A Times UNIV) ensures (B Times UNIV);  \
+Goal "[| i : I;  F i : (A <*> UNIV) ensures (B <*> UNIV);  \
 \        ALL j. F j : preserves snd |] ==>  \
-\     PLam I F : lift_set i (A Times UNIV) ensures lift_set i (B Times UNIV)";
+\     PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)";
 by (auto_tac (claset(), 
 	      simpset() addsimps [ensures_def, lift_transient_eq_disj,
 				  lift_set_Un_distrib RS sym,
@@ -85,11 +85,11 @@
 qed "PLam_ensures";
 
 Goal "[| i : I;  \
-\        F i : ((A Times UNIV) - (B Times UNIV)) co \
-\              ((A Times UNIV) Un (B Times UNIV));  \
-\        F i : transient ((A Times UNIV) - (B Times UNIV));  \
+\        F i : ((A <*> UNIV) - (B <*> UNIV)) co \
+\              ((A <*> UNIV) Un (B <*> UNIV));  \
+\        F i : transient ((A <*> UNIV) - (B <*> UNIV));  \
 \        ALL j. F j : preserves snd |] ==>  \
-\     PLam I F : lift_set i (A Times UNIV) leadsTo lift_set i (B Times UNIV)";
+\     PLam I F : lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)";
 by (rtac (PLam_ensures RS leadsTo_Basis) 1);
 by (rtac ensuresI 2);
 by (ALLGOALS assume_tac);
@@ -98,9 +98,9 @@
 
 (** invariant **)
 
-Goal "[| F i : invariant (A Times UNIV);  i : I;  \
+Goal "[| F i : invariant (A <*> UNIV);  i : I;  \
 \        ALL j. F j : preserves snd |] \
-\     ==> PLam I F : invariant (lift_set i (A Times UNIV))";
+\     ==> PLam I F : invariant (lift_set i (A <*> UNIV))";
 by (auto_tac (claset(),
 	      simpset() addsimps [invariant_def]));
 qed "invariant_imp_PLam_invariant";
diff -r 78b7010db847 -r 816d8f6513be src/HOL/UNITY/TimerArray.ML
--- a/src/HOL/UNITY/TimerArray.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/TimerArray.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -29,7 +29,7 @@
 
 Goal "finite I \
 \     ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}";
-by (eres_inst_tac [("A'1", "%i. lift_set i ({0} Times UNIV)")]
+by (eres_inst_tac [("A'1", "%i. lift_set i ({0} <*> UNIV)")]
     (finite_stable_completion RS leadsTo_weaken) 1);
 by Auto_tac;
 (*Safety property, already reduced to the single Timer case*)
@@ -37,7 +37,7 @@
 (*Progress property for the array of Timers*)
 by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
 by (case_tac "m" 1);
-(*Annoying need to massage the conditions to have the form (... Times UNIV)*)
+(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
 by (auto_tac (claset() addIs [subset_imp_leadsTo], 
 	      simpset() addsimps [insert_absorb, lessThan_Suc RS sym,
 				  lift_set_Un_distrib RS sym,
diff -r 78b7010db847 -r 816d8f6513be src/HOL/UNITY/Token.thy
--- a/src/HOL/UNITY/Token.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/Token.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -58,7 +58,7 @@
   defines
     nodeOrder_def
       "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
-		      (lessThan N Times lessThan N)"
+		      (lessThan N <*> lessThan N)"
 
     next_def
       "next i == (Suc i) mod N"
diff -r 78b7010db847 -r 816d8f6513be src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -14,24 +14,6 @@
 Delsimps [image_Collect];
 
 
-(*** General lemmas ***)
-
-Goal "UNIV Times UNIV = UNIV";
-by Auto_tac;
-qed "UNIV_Times_UNIV"; 
-Addsimps [UNIV_Times_UNIV];
-
-Goal "- (UNIV Times A) = UNIV Times (-A)";
-by Auto_tac;
-qed "Compl_Times_UNIV1"; 
-
-Goal "- (A Times UNIV) = (-A) Times UNIV";
-by Auto_tac;
-qed "Compl_Times_UNIV2"; 
-
-Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; 
-
-
 (*** The abstract type of programs ***)
 
 val rep_ss = simpset() addsimps 
diff -r 78b7010db847 -r 816d8f6513be src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Univ.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -582,7 +582,7 @@
 
 (*** Bounding theorems ***)
 
-Goal "(dprod (A Times B) (C Times D)) <= (uprod A C) Times (uprod B D)";
+Goal "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)";
 by (Blast_tac 1);
 qed "dprod_Sigma";
 
@@ -595,7 +595,7 @@
 by (Blast_tac 1);
 qed "dprod_subset_Sigma2";
 
-Goal "(dsum (A Times B) (C Times D)) <= (usum A C) Times (usum B D)";
+Goal "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)";
 by (Blast_tac 1);
 qed "dsum_Sigma";
 
diff -r 78b7010db847 -r 816d8f6513be src/HOL/WF.ML
--- a/src/HOL/WF.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/WF.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -20,7 +20,7 @@
 
 (*Restriction to domain A.  If r is well-founded over A then wf(r)*)
 val [prem1,prem2] = Goalw [wf_def]
- "[| r <= A Times A;  \
+ "[| r <= A <*> A;  \
 \    !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x);  x:A |] ==> P(x) |]  \
 \ ==>  wf(r)";
 by (blast_tac (claset() addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
diff -r 78b7010db847 -r 816d8f6513be src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/WF_Rel.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -73,7 +73,7 @@
  *---------------------------------------------------------------------------*)
 
 val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
- "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
+ "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)";
 by (EVERY1 [rtac allI,rtac impI]);
 by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
 by (rtac (wfa RS spec RS mp) 1);
@@ -87,7 +87,7 @@
  * Transitivity of WF combinators.
  *---------------------------------------------------------------------------*)
 Goalw [trans_def, lex_prod_def]
-    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)";
+    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)";
 by (Simp_tac 1);
 by (Blast_tac 1);
 qed "trans_lex_prod";
diff -r 78b7010db847 -r 816d8f6513be src/HOL/WF_Rel.thy
--- a/src/HOL/WF_Rel.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/WF_Rel.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -19,7 +19,8 @@
   less_than :: "(nat*nat)set"
   inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
   measure   :: "('a => nat) => ('a * 'a)set"
-  "**"      :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
+  lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
+               (infixr "<*lex*>" 80)
   finite_psubset  :: "('a set * 'a set) set"
 
 
@@ -30,9 +31,8 @@
 
   measure_def   "measure == inv_image less_than"
 
-  lex_prod_def  "ra**rb == {p. ? a a' b b'. 
-                                p = ((a,b),(a',b')) & 
-                               ((a,a') : ra | a=a' & (b,b') : rb)}"
+  lex_prod_def  "ra <*lex*> rb == {((a,b),(a',b')) | a a' b b'.
+                                   ((a,a') : ra | a=a' & (b,b') : rb)}"
 
   (* finite proper subset*)
   finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}"
diff -r 78b7010db847 -r 816d8f6513be src/HOL/ex/Primrec.thy
--- a/src/HOL/ex/Primrec.thy	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/ex/Primrec.thy	Thu Apr 13 15:01:50 2000 +0200
@@ -19,7 +19,7 @@
 Primrec = Main +
 
 consts ack  :: "nat * nat => nat"
-recdef ack "less_than ** less_than"
+recdef ack "less_than <*lex*> less_than"
     "ack (0,n) =  Suc n"
     "ack (Suc m,0) = (ack (m, 1))"
     "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"
diff -r 78b7010db847 -r 816d8f6513be src/HOL/ex/Tarski.ML
--- a/src/HOL/ex/Tarski.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/ex/Tarski.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -540,7 +540,7 @@
 qed "T_thm_1_glb";
 
 (* interval *)
-Goal "refl A r ==> r <= A Times A";
+Goal "refl A r ==> r <= A <*> A";
 by (afs [refl_def] 1);
 qed "reflE1";