Times -> <*>
authornipkow
Thu Apr 13 15:01:50 2000 +0200 (2000-04-13)
changeset 8703816d8f6513be
parent 8702 78b7010db847
child 8704 f76f41f24c44
Times -> <*>
** -> <*lex*>
src/HOL/BCV/SemiLattice.ML
src/HOL/Induct/LList.ML
src/HOL/Induct/Mutil.ML
src/HOL/Integ/Equiv.ML
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Lex/AutoChopper1.thy
src/HOL/List.thy
src/HOL/Prod.ML
src/HOL/Prod.thy
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
src/HOL/Real/HahnBanach/Linearform.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
src/HOL/Relation.ML
src/HOL/Relation.thy
src/HOL/Sexp.ML
src/HOL/Subst/Unify.thy
src/HOL/Trancl.ML
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/LessThan.thy
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/PPROD.ML
src/HOL/UNITY/TimerArray.ML
src/HOL/UNITY/Token.thy
src/HOL/UNITY/UNITY.ML
src/HOL/Univ.ML
src/HOL/WF.ML
src/HOL/WF_Rel.ML
src/HOL/WF_Rel.thy
src/HOL/ex/Primrec.thy
src/HOL/ex/Tarski.ML
     1.1 --- a/src/HOL/BCV/SemiLattice.ML	Thu Apr 13 15:01:45 2000 +0200
     1.2 +++ b/src/HOL/BCV/SemiLattice.ML	Thu Apr 13 15:01:50 2000 +0200
     1.3 @@ -150,6 +150,6 @@
     1.4  
     1.5  (* product *)
     1.6  
     1.7 -Goalw [semilat_def,plus_prod] "[| semilat A; semilat B |] ==> semilat (A Times B)";
     1.8 +Goalw [semilat_def,plus_prod] "[| semilat A; semilat B |] ==> semilat (A <*> B)";
     1.9  by (Asm_simp_tac 1);
    1.10  qed "semilat_Times";
     2.1 --- a/src/HOL/Induct/LList.ML	Thu Apr 13 15:01:45 2000 +0200
     2.2 +++ b/src/HOL/Induct/LList.ML	Thu Apr 13 15:01:50 2000 +0200
     2.3 @@ -616,20 +616,20 @@
     2.4  (*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
     2.5  
     2.6  Goalw [LListD_Fun_def]
     2.7 -    "r <= (llist A) Times (llist A) ==> \
     2.8 -\           LListD_Fun (diag A) r <= (llist A) Times (llist A)";
     2.9 +    "r <= (llist A) <*> (llist A) ==> \
    2.10 +\           LListD_Fun (diag A) r <= (llist A) <*> (llist A)";
    2.11  by (stac llist_unfold 1);
    2.12  by (simp_tac (simpset() addsimps [NIL_def, CONS_def]) 1);
    2.13  by (Fast_tac 1);
    2.14  qed "LListD_Fun_subset_Times_llist";
    2.15  
    2.16  Goal "prod_fun Rep_LList Rep_LList `` r <= \
    2.17 -\    (llist(range Leaf)) Times (llist(range Leaf))";
    2.18 +\    (llist(range Leaf)) <*> (llist(range Leaf))";
    2.19  by (fast_tac (claset() delrules [image_subsetI]
    2.20  		       addIs [Rep_LList RS LListD]) 1);
    2.21  qed "subset_Times_llist";
    2.22  
    2.23 -Goal "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
    2.24 +Goal "r <= (llist(range Leaf)) <*> (llist(range Leaf)) ==> \
    2.25  \    prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) `` r <= r";
    2.26  by Safe_tac;
    2.27  by (etac (subsetD RS SigmaE2) 1);
     3.1 --- a/src/HOL/Induct/Mutil.ML	Thu Apr 13 15:01:45 2000 +0200
     3.2 +++ b/src/HOL/Induct/Mutil.ML	Thu Apr 13 15:01:50 2000 +0200
     3.3 @@ -32,22 +32,22 @@
     3.4  Addsimps [below_0];
     3.5  
     3.6  Goalw [below_def]
     3.7 -    "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
     3.8 +    "below(Suc n) <*> B = ({n} <*> B) Un ((below n) <*> B)";
     3.9  by Auto_tac;
    3.10  qed "Sigma_Suc1";
    3.11  
    3.12  Goalw [below_def]
    3.13 -    "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
    3.14 +    "A <*> below(Suc n) = (A <*> {n}) Un (A <*> (below n))";
    3.15  by Auto_tac;
    3.16  qed "Sigma_Suc2";
    3.17  
    3.18  Addsimps [Sigma_Suc1, Sigma_Suc2];
    3.19  
    3.20 -Goal "({i} Times {n}) Un ({i} Times {m}) = {(i,m), (i,n)}";
    3.21 +Goal "({i} <*> {n}) Un ({i} <*> {m}) = {(i,m), (i,n)}";
    3.22  by Auto_tac;
    3.23  qed "sing_Times_lemma";
    3.24  
    3.25 -Goal "{i} Times below(n+n) : tiling domino";
    3.26 +Goal "{i} <*> below(n+n) : tiling domino";
    3.27  by (induct_tac "n" 1);
    3.28  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym])));
    3.29  by (rtac tiling.Un 1);
    3.30 @@ -56,7 +56,7 @@
    3.31  
    3.32  AddSIs [dominoes_tile_row]; 
    3.33  
    3.34 -Goal "(below m) Times below(n+n) : tiling domino";
    3.35 +Goal "(below m) <*> below(n+n) : tiling domino";
    3.36  by (induct_tac "m" 1);
    3.37  by Auto_tac;
    3.38  qed "dominoes_tile_matrix";
    3.39 @@ -121,7 +121,7 @@
    3.40  qed "gen_mutil_not_tiling";
    3.41  
    3.42  (*Apply the general theorem to the well-known case*)
    3.43 -Goal "[| t = below(Suc m + Suc m) Times below(Suc n + Suc n) |] \
    3.44 +Goal "[| t = below(Suc m + Suc m) <*> below(Suc n + Suc n) |] \
    3.45  \     ==> t - {(0,0)} - {(Suc(m+m), Suc(n+n))} ~: tiling domino";
    3.46  by (rtac gen_mutil_not_tiling 1);
    3.47  by (blast_tac (claset() addSIs [dominoes_tile_matrix]) 1);
     4.1 --- a/src/HOL/Integ/Equiv.ML	Thu Apr 13 15:01:45 2000 +0200
     4.2 +++ b/src/HOL/Integ/Equiv.ML	Thu Apr 13 15:01:50 2000 +0200
     4.3 @@ -73,7 +73,7 @@
     4.4  qed "equiv_class_nondisjoint";
     4.5  
     4.6  val [major] = goalw Equiv.thy [equiv_def,refl_def]
     4.7 -    "equiv A r ==> r <= A Times A";
     4.8 +    "equiv A r ==> r <= A <*> A";
     4.9  by (rtac (major RS conjunct1 RS conjunct1) 1);
    4.10  qed "equiv_type";
    4.11  
    4.12 @@ -241,8 +241,8 @@
    4.13  
    4.14  (*** Cardinality results suggested by Florian Kammueller ***)
    4.15  
    4.16 -(*Recall that  equiv A r  implies  r <= A Times A   (equiv_type) *)
    4.17 -Goal "[| finite A; r <= A Times A |] ==> finite (A/r)";
    4.18 +(*Recall that  equiv A r  implies  r <= A <*> A   (equiv_type) *)
    4.19 +Goal "[| finite A; r <= A <*> A |] ==> finite (A/r)";
    4.20  by (rtac finite_subset 1);
    4.21  by (etac (finite_Pow_iff RS iffD2) 2);
    4.22  by (rewtac quotient_def);
    4.23 @@ -250,7 +250,7 @@
    4.24  qed "finite_quotient";
    4.25  
    4.26  Goalw [quotient_def]
    4.27 -    "[| finite A;  r <= A Times A;  X : A/r |] ==> finite X";
    4.28 +    "[| finite A;  r <= A <*> A;  X : A/r |] ==> finite X";
    4.29  by (rtac finite_subset 1);
    4.30  by (assume_tac 2);
    4.31  by (Blast_tac 1);
     5.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Apr 13 15:01:45 2000 +0200
     5.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Apr 13 15:01:50 2000 +0200
     5.3 @@ -67,11 +67,11 @@
     5.4    by (simp add: below_def);
     5.5  
     5.6  lemma Sigma_Suc1:
     5.7 -    "below (Suc n) Times B = ({n} Times B) Un (below n Times B)";
     5.8 +    "below (Suc n) <*> B = ({n} <*> B) Un (below n <*> B)";
     5.9    by (simp add: below_def less_Suc_eq) blast;
    5.10  
    5.11  lemma Sigma_Suc2:
    5.12 -    "A Times below (Suc n) = (A Times {n}) Un (A Times (below n))";
    5.13 +    "A <*> below (Suc n) = (A <*> {n}) Un (A <*> (below n))";
    5.14    by (simp add: below_def less_Suc_eq) blast;
    5.15  
    5.16  lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2;
    5.17 @@ -122,13 +122,13 @@
    5.18      vertl:  "{(i, j), (i + 1, j)} : domino";
    5.19  
    5.20  lemma dominoes_tile_row:
    5.21 -  "{i} Times below (2 * n) : tiling domino"
    5.22 +  "{i} <*> below (2 * n) : tiling domino"
    5.23    (is "?P n" is "?B n : ?T");
    5.24  proof (induct n);
    5.25    show "?P 0"; by (simp add: below_0 tiling.empty);
    5.26  
    5.27    fix n; assume hyp: "?P n";
    5.28 -  let ?a = "{i} Times {2 * n + 1} Un {i} Times {2 * n}";
    5.29 +  let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}";
    5.30  
    5.31    have "?B (Suc n) = ?a Un ?B n"; by (simp add: Sigma_Suc Un_assoc);
    5.32    also; have "... : ?T";
    5.33 @@ -144,13 +144,13 @@
    5.34  qed;
    5.35  
    5.36  lemma dominoes_tile_matrix:
    5.37 -  "below m Times below (2 * n) : tiling domino"
    5.38 +  "below m <*> below (2 * n) : tiling domino"
    5.39    (is "?P m" is "?B m : ?T");
    5.40  proof (induct m);
    5.41    show "?P 0"; by (simp add: below_0 tiling.empty);
    5.42  
    5.43    fix m; assume hyp: "?P m";
    5.44 -  let ?t = "{m} Times below (2 * n)";
    5.45 +  let ?t = "{m} <*> below (2 * n)";
    5.46  
    5.47    have "?B (Suc m) = ?t Un ?B m"; by (simp add: Sigma_Suc);
    5.48    also; have "... : ?T";
    5.49 @@ -249,13 +249,13 @@
    5.50  constdefs
    5.51    mutilated_board :: "nat => nat => (nat * nat) set"
    5.52    "mutilated_board m n ==
    5.53 -    below (2 * (m + 1)) Times below (2 * (n + 1))
    5.54 +    below (2 * (m + 1)) <*> below (2 * (n + 1))
    5.55        - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}";
    5.56  
    5.57  theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino";
    5.58  proof (unfold mutilated_board_def);
    5.59    let ?T = "tiling domino";
    5.60 -  let ?t = "below (2 * (m + 1)) Times below (2 * (n + 1))";
    5.61 +  let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))";
    5.62    let ?t' = "?t - {(0, 0)}";
    5.63    let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}";
    5.64  
     6.1 --- a/src/HOL/Lex/AutoChopper1.thy	Thu Apr 13 15:01:45 2000 +0200
     6.2 +++ b/src/HOL/Lex/AutoChopper1.thy	Thu Apr 13 15:01:50 2000 +0200
     6.3 @@ -22,7 +22,7 @@
     6.4  consts
     6.5    acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)
     6.6            => 'a list list * 'a list"
     6.7 -recdef acc "inv_image (less_than ** less_than)
     6.8 +recdef acc "inv_image (less_than <*lex*> less_than)
     6.9                (%(A,ys,s,xss,zs,xs). (length xs + length ys + length zs,
    6.10                                       length ys))"
    6.11  "acc(A,[],s,xss,zs,[]) = (xss, zs)"
     7.1 --- a/src/HOL/List.thy	Thu Apr 13 15:01:45 2000 +0200
     7.2 +++ b/src/HOL/List.thy	Thu Apr 13 15:01:50 2000 +0200
     7.3 @@ -176,7 +176,7 @@
     7.4   lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
     7.5  primrec
     7.6  "lexn r 0       = {}"
     7.7 -"lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r ** lexn r n)) Int
     7.8 +"lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r <*lex*> lexn r n)) Int
     7.9                    {(xs,ys). length xs = Suc n & length ys = Suc n}"
    7.10  
    7.11  constdefs
    7.12 @@ -184,7 +184,7 @@
    7.13  "lex r == UN n. lexn r n"
    7.14  
    7.15   lexico :: "('a * 'a)set => ('a list * 'a list)set"
    7.16 -"lexico r == inv_image (less_than ** lex r) (%xs. (length xs, xs))"
    7.17 +"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
    7.18  
    7.19  end
    7.20  
     8.1 --- a/src/HOL/Prod.ML	Thu Apr 13 15:01:45 2000 +0200
     8.2 +++ b/src/HOL/Prod.ML	Thu Apr 13 15:01:50 2000 +0200
     8.3 @@ -401,22 +401,37 @@
     8.4  by (Blast_tac 1) ;
     8.5  qed "Sigma_empty1";
     8.6  
     8.7 -Goal "A Times {} = {}";
     8.8 +Goal "A <*> {} = {}";
     8.9  by (Blast_tac 1) ;
    8.10  qed "Sigma_empty2";
    8.11  
    8.12 -Addsimps [Sigma_empty1,Sigma_empty2]; 
    8.13 +Addsimps [Sigma_empty1,Sigma_empty2];
    8.14 +
    8.15 +Goal "UNIV <*> UNIV = UNIV";
    8.16 +by Auto_tac;
    8.17 +qed "UNIV_Times_UNIV"; 
    8.18 +Addsimps [UNIV_Times_UNIV];
    8.19 +
    8.20 +Goal "- (UNIV <*> A) = UNIV <*> (-A)";
    8.21 +by Auto_tac;
    8.22 +qed "Compl_Times_UNIV1"; 
    8.23 +
    8.24 +Goal "- (A <*> UNIV) = (-A) <*> UNIV";
    8.25 +by Auto_tac;
    8.26 +qed "Compl_Times_UNIV2"; 
    8.27 +
    8.28 +Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; 
    8.29  
    8.30  Goal "((a,b): Sigma A B) = (a:A & b:B(a))";
    8.31  by (Blast_tac 1);
    8.32  qed "mem_Sigma_iff";
    8.33  AddIffs [mem_Sigma_iff]; 
    8.34  
    8.35 -Goal "x:C ==> (A Times C <= B Times C) = (A <= B)";
    8.36 +Goal "x:C ==> (A <*> C <= B <*> C) = (A <= B)";
    8.37  by (Blast_tac 1);
    8.38  qed "Times_subset_cancel2";
    8.39  
    8.40 -Goal "x:C ==> (A Times C = B Times C) = (A = B)";
    8.41 +Goal "x:C ==> (A <*> C = B <*> C) = (A = B)";
    8.42  by (blast_tac (claset() addEs [equalityE]) 1);
    8.43  qed "Times_eq_cancel2";
    8.44  
    8.45 @@ -426,14 +441,14 @@
    8.46  
    8.47  (*** Complex rules for Sigma ***)
    8.48  
    8.49 -Goal "{(a,b). P a & Q b} = Collect P Times Collect Q";
    8.50 +Goal "{(a,b). P a & Q b} = Collect P <*> Collect Q";
    8.51  by (Blast_tac 1);
    8.52  qed "Collect_split";
    8.53  
    8.54  Addsimps [Collect_split];
    8.55  
    8.56  (*Suggested by Pierre Chartier*)
    8.57 -Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
    8.58 +Goal "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)";
    8.59  by (Blast_tac 1);
    8.60  qed "UN_Times_distrib";
    8.61  
    8.62 @@ -477,15 +492,15 @@
    8.63  
    8.64  (*Non-dependent versions are needed to avoid the need for higher-order
    8.65    matching, especially when the rules are re-oriented*)
    8.66 -Goal "(A Un B) Times C = (A Times C) Un (B Times C)";
    8.67 +Goal "(A Un B) <*> C = (A <*> C) Un (B <*> C)";
    8.68  by (Blast_tac 1);
    8.69  qed "Times_Un_distrib1"; 
    8.70  
    8.71 -Goal "(A Int B) Times C = (A Times C) Int (B Times C)";
    8.72 +Goal "(A Int B) <*> C = (A <*> C) Int (B <*> C)";
    8.73  by (Blast_tac 1);
    8.74  qed "Times_Int_distrib1"; 
    8.75  
    8.76 -Goal "(A - B) Times C = (A Times C) - (B Times C)";
    8.77 +Goal "(A - B) <*> C = (A <*> C) - (B <*> C)";
    8.78  by (Blast_tac 1);
    8.79  qed "Times_Diff_distrib1"; 
    8.80  
     9.1 --- a/src/HOL/Prod.thy	Thu Apr 13 15:01:45 2000 +0200
     9.2 +++ b/src/HOL/Prod.thy	Thu Apr 13 15:01:50 2000 +0200
     9.3 @@ -55,7 +55,7 @@
     9.4    "_patterns"   :: [pttrn, patterns] => patterns ("_,/_")
     9.5  
     9.6    "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
     9.7 -  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ Times _" [81, 80] 80)
     9.8 +  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    (infixr "<*>" 80)
     9.9  
    9.10  translations
    9.11    "(x, y, z)"    == "(x, (y, z))"
    9.12 @@ -68,7 +68,7 @@
    9.13       The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
    9.14  
    9.15    "SIGMA x:A. B" => "Sigma A (%x. B)"
    9.16 -  "A Times B"    => "Sigma A (_K B)"
    9.17 +  "A <*> B"      => "Sigma A (_K B)"
    9.18  
    9.19  syntax (symbols)
    9.20    "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
    10.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Apr 13 15:01:45 2000 +0200
    10.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Apr 13 15:01:50 2000 +0200
    10.3 @@ -66,7 +66,7 @@
    10.4  constdefs
    10.5    B :: "[ 'a set, 'a => real, 'a => real ] => real set"
    10.6    "B V norm f == 
    10.7 -  {0r} \Un {rabs (f x) * rinv (norm x) | x. x ~= <0> & x:V}";
    10.8 +  {0r} \Un {rabs (f x) * rinv (norm x) | x. x ~= 00 & x:V}";
    10.9  
   10.10  text{* $n$ is the function norm of $f$, iff 
   10.11  $n$ is the supremum of $B$. 
   10.12 @@ -141,7 +141,7 @@
   10.13  
   10.14        next;
   10.15  	fix x y;
   10.16 -        assume "x:V" "x ~= <0>"; (***
   10.17 +        assume "x:V" "x ~= 00"; (***
   10.18  
   10.19           have ge: "0r <= rinv (norm x)";
   10.20            by (rule real_less_imp_le, rule real_rinv_gt_zero, 
   10.21 @@ -207,7 +207,7 @@
   10.22      proof (intro ballI, unfold B_def,
   10.23             elim UnE singletonE CollectE exE conjE); 
   10.24        fix x r;
   10.25 -      assume "x : V" "x ~= <0>" 
   10.26 +      assume "x : V" "x ~= 00" 
   10.27          and r: "r = rabs (f x) * rinv (norm x)";
   10.28  
   10.29        have ge: "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero);
   10.30 @@ -259,9 +259,9 @@
   10.31      from the linearity of $f$: for every linear function
   10.32      holds $f\ap \zero = 0$. *};
   10.33  
   10.34 -    assume "x = <0>";
   10.35 -    have "rabs (f x) = rabs (f <0>)"; by (simp!);
   10.36 -    also; from v continuous_linearform; have "f <0> = 0r"; ..;
   10.37 +    assume "x = 00";
   10.38 +    have "rabs (f x) = rabs (f 00)"; by (simp!);
   10.39 +    also; from v continuous_linearform; have "f 00 = 0r"; ..;
   10.40      also; note rabs_zero;
   10.41      also; have "0r <= function_norm V norm f * norm x";
   10.42      proof (rule real_le_mult_order);
   10.43 @@ -272,7 +272,7 @@
   10.44      show "rabs (f x) <= function_norm V norm f * norm x"; .;
   10.45  
   10.46    next;
   10.47 -    assume "x ~= <0>";
   10.48 +    assume "x ~= 00";
   10.49      have n: "0r <= norm x"; ..;
   10.50      have nz: "norm x ~= 0r";
   10.51      proof (rule lt_imp_not_eq [RS not_sym]);
   10.52 @@ -356,7 +356,7 @@
   10.53  
   10.54        next;
   10.55  	fix x; 
   10.56 -        assume "x : V" "x ~= <0>"; 
   10.57 +        assume "x : V" "x ~= 00"; 
   10.58  
   10.59          have lz: "0r < norm x"; 
   10.60            by (simp! add: normed_vs_norm_gt_zero);
    11.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Apr 13 15:01:45 2000 +0200
    11.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Apr 13 15:01:50 2000 +0200
    11.3 @@ -145,9 +145,9 @@
    11.4              qed;
    11.5              thus ?thesis; by blast;
    11.6            qed;
    11.7 -          have x0: "x0 ~= <0>";
    11.8 +          have x0: "x0 ~= 00";
    11.9            proof (rule classical);
   11.10 -            presume "x0 = <0>";
   11.11 +            presume "x0 = 00";
   11.12              with h; have "x0:H"; by simp;
   11.13              thus ?thesis; by contradiction;
   11.14            qed blast;
   11.15 @@ -190,7 +190,7 @@
   11.16  
   11.17  txt {* Define the extension $h_0$ of $h$ to $H_0$ using $\xi$.  *};
   11.18  
   11.19 -            def h0 == "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 
   11.20 +            def h0 == "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a (*) x0 
   11.21                                                    & y:H
   11.22                             in (h y) + a * xi";
   11.23              show ?thesis;
   11.24 @@ -205,7 +205,7 @@
   11.25  		  have  "graph H h <= graph H0 h0";
   11.26                    proof (rule graph_extI);
   11.27  		    fix t; assume "t:H"; 
   11.28 -		    have "(SOME (y, a). t = y + a <*> x0 & y : H)
   11.29 +		    have "(SOME (y, a). t = y + a (*) x0 & y : H)
   11.30                           = (t,0r)";
   11.31  		      by (rule decomp_H0_H [OF _ _ _ _ _ x0]);
   11.32  		    thus "h t = h0 t"; by (simp! add: Let_def);
   11.33 @@ -228,8 +228,8 @@
   11.34  		    assume e: "graph H h = graph H0 h0";
   11.35  		    have "x0 : H0"; 
   11.36  		    proof (unfold H0_def, rule vs_sumI);
   11.37 -		      show "x0 = <0> + x0"; by (simp!);
   11.38 -		      from h; show "<0> : H"; ..;
   11.39 +		      show "x0 = 00 + x0"; by (simp!);
   11.40 +		      from h; show "00 : H"; ..;
   11.41  		      show "x0 : lin x0"; by (rule x_lin_x);
   11.42  		    qed;
   11.43  		    hence "(x0, h0 x0) : graph H0 h0"; ..;
   11.44 @@ -265,10 +265,10 @@
   11.45  		    also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
   11.46  		      by (simp add: Let_def);
   11.47  		    also; have 
   11.48 -		      "(x, 0r) = (SOME (y, a). x = y + a <*> x0 & y : H)";
   11.49 +		      "(x, 0r) = (SOME (y, a). x = y + a (*) x0 & y : H)";
   11.50  		      by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x0]) (simp!)+;
   11.51  		    also; have 
   11.52 -		      "(let (y,a) = (SOME (y,a). x = y + a <*> x0 & y : H)
   11.53 +		      "(let (y,a) = (SOME (y,a). x = y + a (*) x0 & y : H)
   11.54                          in h y + a * xi) 
   11.55                        = h0 x"; by (simp!);
   11.56  		    finally; show "f x = h0 x"; .;
   11.57 @@ -427,9 +427,9 @@
   11.58    proof;
   11.59      fix x0; assume "x0:E" "x0~:H";
   11.60  
   11.61 -    have x0: "x0 ~= <0>";
   11.62 +    have x0: "x0 ~= 00";
   11.63      proof (rule classical);
   11.64 -      presume "x0 = <0>";
   11.65 +      presume "x0 = 00";
   11.66        with h; have "x0:H"; by simp;
   11.67        thus ?thesis; by contradiction;
   11.68      qed blast;
   11.69 @@ -471,7 +471,7 @@
   11.70        of $h$ on $H_0$:*};  
   11.71  
   11.72        def h0 ==
   11.73 -          "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 & y:H
   11.74 +          "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a ( * ) x0 & y:H
   11.75                 in (h y) + a * xi";
   11.76  
   11.77        txt {* We get that the graph of $h_0$ extends that of
   11.78 @@ -480,7 +480,7 @@
   11.79        have  "graph H h <= graph H0 h0"; 
   11.80        proof (rule graph_extI);
   11.81          fix t; assume "t:H"; 
   11.82 -        have "(SOME (y, a). t = y + a <*> x0 & y : H) = (t,0r)";
   11.83 +        have "(SOME (y, a). t = y + a ( * ) x0 & y : H) = (t,0r)";
   11.84            by (rule decomp_H0_H, rule x0); 
   11.85          thus "h t = h0 t"; by (simp! add: Let_def);
   11.86        next;
   11.87 @@ -502,8 +502,8 @@
   11.88          assume e: "graph H h = graph H0 h0";
   11.89          have "x0 : H0"; 
   11.90          proof (unfold H0_def, rule vs_sumI);
   11.91 -          show "x0 = <0> + x0"; by (simp!);
   11.92 -          from h; show "<0> : H"; ..;
   11.93 +          show "x0 = 00 + x0"; by (simp!);
   11.94 +          from h; show "00 : H"; ..;
   11.95            show "x0 : lin x0"; by (rule x_lin_x);
   11.96          qed;
   11.97          hence "(x0, h0 x0) : graph H0 h0"; ..;
   11.98 @@ -545,10 +545,10 @@
   11.99            also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
  11.100              by (simp add: Let_def);
  11.101            also; have 
  11.102 -            "(x, 0r) = (SOME (y, a). x = y + a <*> x0 & y : H)";
  11.103 +            "(x, 0r) = (SOME (y, a). x = y + a ( * ) x0 & y : H)";
  11.104              by (rule decomp_H0_H [RS sym], rule x0) (simp!)+;
  11.105            also; have 
  11.106 -            "(let (y,a) = (SOME (y,a). x = y + a <*> x0 & y : H)
  11.107 +            "(let (y,a) = (SOME (y,a). x = y + a ( * ) x0 & y : H)
  11.108                in h y + a * xi) 
  11.109               = h0 x"; by (simp!);
  11.110            finally; show "f x = h0 x"; .;
  11.111 @@ -672,11 +672,11 @@
  11.112  
  11.113      txt{* $p$ is absolutely homogenous: *};
  11.114  
  11.115 -    show "p (a <*> x) = rabs a * p x";
  11.116 +    show "p (a (*) x) = rabs a * p x";
  11.117      proof -; 
  11.118 -      have "p (a <*> x) = function_norm F norm f * norm (a <*> x)";
  11.119 +      have "p (a (*) x) = function_norm F norm f * norm (a (*) x)";
  11.120          by (simp!);
  11.121 -      also; have "norm (a <*> x) = rabs a * norm x"; 
  11.122 +      also; have "norm (a (*) x) = rabs a * norm x"; 
  11.123          by (rule normed_vs_norm_rabs_homogenous);
  11.124        also; have "function_norm F norm f * (rabs a * norm x) 
  11.125          = rabs a * (function_norm F norm f * norm x)";
  11.126 @@ -801,4 +801,4 @@
  11.127    qed;
  11.128  qed;
  11.129  
  11.130 -end;
  11.131 \ No newline at end of file
  11.132 +end;
    12.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Apr 13 15:01:45 2000 +0200
    12.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Apr 13 15:01:50 2000 +0200
    12.3 @@ -52,27 +52,27 @@
    12.4    
    12.5      txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
    12.6  
    12.7 -    from vs; have "a <0> : ?S"; by force;
    12.8 +    from vs; have "a 00 : ?S"; by force;
    12.9      thus "EX X. X : ?S"; ..;
   12.10  
   12.11      txt {* $b\ap \zero$ is an upper bound of $S$: *};
   12.12  
   12.13      show "EX Y. isUb UNIV ?S Y"; 
   12.14      proof; 
   12.15 -      show "isUb UNIV ?S (b <0>)";
   12.16 +      show "isUb UNIV ?S (b 00)";
   12.17        proof (intro isUbI setleI ballI);
   12.18 -        show "b <0> : UNIV"; ..;
   12.19 +        show "b 00 : UNIV"; ..;
   12.20        next;
   12.21  
   12.22          txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
   12.23  
   12.24          fix y; assume y: "y : ?S"; 
   12.25          from y; have "EX u:F. y = a u"; by fast;
   12.26 -        thus "y <= b <0>"; 
   12.27 +        thus "y <= b 00"; 
   12.28          proof;
   12.29            fix u; assume "u:F"; 
   12.30            assume "y = a u";
   12.31 -          also; have "a u <= b <0>"; by (rule r) (simp!)+;
   12.32 +          also; have "a u <= b 00"; by (rule r) (simp!)+;
   12.33            finally; show ?thesis; .;
   12.34          qed;
   12.35        qed;
   12.36 @@ -121,18 +121,18 @@
   12.37  is a linear extension of $h$ to $H_0$. *};
   12.38  
   12.39  lemma h0_lf: 
   12.40 -  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
   12.41 +  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H 
   12.42                  in h y + a * xi);
   12.43    H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H; 
   12.44 -  x0 : E; x0 ~= <0>; is_vectorspace E |]
   12.45 +  x0 : E; x0 ~= 00; is_vectorspace E |]
   12.46    ==> is_linearform H0 h0";
   12.47  proof -;
   12.48    assume h0_def: 
   12.49 -    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
   12.50 +    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H 
   12.51                 in h y + a * xi)"
   12.52      and H0_def: "H0 == H + lin x0" 
   12.53      and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
   12.54 -      "x0 ~= <0>" "x0 : E" "is_vectorspace E";
   12.55 +      "x0 ~= 00" "x0 : E" "is_vectorspace E";
   12.56  
   12.57    have h0: "is_vectorspace H0"; 
   12.58    proof (unfold H0_def, rule vs_sum_vs);
   12.59 @@ -150,27 +150,27 @@
   12.60      have x1x2: "x1 + x2 : H0"; 
   12.61        by (rule vs_add_closed, rule h0); 
   12.62      from x1; 
   12.63 -    have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0  & y1 : H"; 
   12.64 +    have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0  & y1 : H"; 
   12.65        by (unfold H0_def vs_sum_def lin_def) fast;
   12.66      from x2; 
   12.67 -    have ex_x2: "EX y2 a2. x2 = y2 + a2 <*> x0 & y2 : H"; 
   12.68 +    have ex_x2: "EX y2 a2. x2 = y2 + a2 (*) x0 & y2 : H"; 
   12.69        by (unfold H0_def vs_sum_def lin_def) fast;
   12.70      from x1x2; 
   12.71 -    have ex_x1x2: "EX y a. x1 + x2 = y + a <*> x0 & y : H";
   12.72 +    have ex_x1x2: "EX y a. x1 + x2 = y + a (*) x0 & y : H";
   12.73        by (unfold H0_def vs_sum_def lin_def) fast;
   12.74  
   12.75      from ex_x1 ex_x2 ex_x1x2;
   12.76      show "h0 (x1 + x2) = h0 x1 + h0 x2";
   12.77      proof (elim exE conjE);
   12.78        fix y1 y2 y a1 a2 a;
   12.79 -      assume y1: "x1 = y1 + a1 <*> x0"     and y1': "y1 : H"
   12.80 -         and y2: "x2 = y2 + a2 <*> x0"     and y2': "y2 : H" 
   12.81 -         and y: "x1 + x2 = y + a <*> x0"   and y':  "y  : H"; 
   12.82 +      assume y1: "x1 = y1 + a1 (*) x0"     and y1': "y1 : H"
   12.83 +         and y2: "x2 = y2 + a2 (*) x0"     and y2': "y2 : H" 
   12.84 +         and y: "x1 + x2 = y + a (*) x0"   and y':  "y  : H"; 
   12.85  
   12.86        have ya: "y1 + y2 = y & a1 + a2 = a"; 
   12.87        proof (rule decomp_H0);;
   12.88  	txt_raw {* \label{decomp-H0-use} *};;
   12.89 -        show "y1 + y2 + (a1 + a2) <*> x0 = y + a <*> x0"; 
   12.90 +        show "y1 + y2 + (a1 + a2) (*) x0 = y + a (*) x0"; 
   12.91            by (simp! add: vs_add_mult_distrib2 [of E]);
   12.92          show "y1 + y2 : H"; ..;
   12.93        qed;
   12.94 @@ -199,31 +199,31 @@
   12.95  
   12.96    next;  
   12.97      fix c x1; assume x1: "x1 : H0";    
   12.98 -    have ax1: "c <*> x1 : H0";
   12.99 +    have ax1: "c (*) x1 : H0";
  12.100        by (rule vs_mult_closed, rule h0);
  12.101      from x1; have ex_x: "!! x. x: H0 
  12.102 -                        ==> EX y a. x = y + a <*> x0 & y : H";
  12.103 +                        ==> EX y a. x = y + a (*) x0 & y : H";
  12.104        by (unfold H0_def vs_sum_def lin_def) fast;
  12.105  
  12.106 -    from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
  12.107 +    from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H";
  12.108        by (unfold H0_def vs_sum_def lin_def) fast;
  12.109 -    with ex_x [of "c <*> x1", OF ax1];
  12.110 -    show "h0 (c <*> x1) = c * (h0 x1)";  
  12.111 +    with ex_x [of "c (*) x1", OF ax1];
  12.112 +    show "h0 (c (*) x1) = c * (h0 x1)";  
  12.113      proof (elim exE conjE);
  12.114        fix y1 y a1 a; 
  12.115 -      assume y1: "x1 = y1 + a1 <*> x0"       and y1': "y1 : H"
  12.116 -        and y: "c <*> x1 = y  + a  <*> x0"   and y':  "y  : H"; 
  12.117 +      assume y1: "x1 = y1 + a1 (*) x0"       and y1': "y1 : H"
  12.118 +        and y: "c (*) x1 = y  + a  (*) x0"   and y':  "y  : H"; 
  12.119  
  12.120 -      have ya: "c <*> y1 = y & c * a1 = a"; 
  12.121 +      have ya: "c (*) y1 = y & c * a1 = a"; 
  12.122        proof (rule decomp_H0); 
  12.123 -	show "c <*> y1 + (c * a1) <*> x0 = y + a <*> x0"; 
  12.124 +	show "c (*) y1 + (c * a1) (*) x0 = y + a (*) x0"; 
  12.125            by (simp! add: add: vs_add_mult_distrib1);
  12.126 -        show "c <*> y1 : H"; ..;
  12.127 +        show "c (*) y1 : H"; ..;
  12.128        qed;
  12.129  
  12.130 -      have "h0 (c <*> x1) = h y + a * xi"; 
  12.131 +      have "h0 (c (*) x1) = h y + a * xi"; 
  12.132  	by (rule h0_definite);
  12.133 -      also; have "... = h (c <*> y1) + (c * a1) * xi";
  12.134 +      also; have "... = h (c (*) y1) + (c * a1) * xi";
  12.135          by (simp add: ya);
  12.136        also; from vs y1'; have "... = c * h y1 + c * a1 * xi"; 
  12.137  	by (simp add: linearform_mult [of H]);
  12.138 @@ -240,31 +240,31 @@
  12.139  is bounded by the seminorm $p$. *};
  12.140  
  12.141  lemma h0_norm_pres:
  12.142 -  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
  12.143 +  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H 
  12.144                  in h y + a * xi);
  12.145 -  H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E; 
  12.146 +  H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= 00; is_vectorspace E; 
  12.147    is_subspace H E; is_seminorm E p; is_linearform H h; ALL y:H. h y <= p y; 
  12.148    ALL y:H. - p (y + x0) - h y <= xi & xi <= p (y + x0) - h y |]
  12.149     ==> ALL x:H0. h0 x <= p x"; 
  12.150  proof; 
  12.151    assume h0_def: 
  12.152 -    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
  12.153 +    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H 
  12.154                 in (h y) + a * xi)"
  12.155      and H0_def: "H0 == H + lin x0" 
  12.156 -    and vs: "x0 ~: H" "x0 : E" "x0 ~= <0>" "is_vectorspace E" 
  12.157 +    and vs: "x0 ~: H" "x0 : E" "x0 ~= 00" "is_vectorspace E" 
  12.158              "is_subspace H E" "is_seminorm E p" "is_linearform H h" 
  12.159      and a: "ALL y:H. h y <= p y";
  12.160    presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi";
  12.161    presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya";
  12.162    fix x; assume "x : H0"; 
  12.163    have ex_x: 
  12.164 -    "!! x. x : H0 ==> EX y a. x = y + a <*> x0 & y : H";
  12.165 +    "!! x. x : H0 ==> EX y a. x = y + a (*) x0 & y : H";
  12.166      by (unfold H0_def vs_sum_def lin_def) fast;
  12.167 -  have "EX y a. x = y + a <*> x0 & y : H";
  12.168 +  have "EX y a. x = y + a (*) x0 & y : H";
  12.169      by (rule ex_x);
  12.170    thus "h0 x <= p x";
  12.171    proof (elim exE conjE);
  12.172 -    fix y a; assume x: "x = y + a <*> x0" and y: "y : H";
  12.173 +    fix y a; assume x: "x = y + a (*) x0" and y: "y : H";
  12.174      have "h0 x = h y + a * xi";
  12.175        by (rule h0_definite);
  12.176  
  12.177 @@ -272,7 +272,7 @@
  12.178      $h\ap y + a \cdot \xi\leq  p\ap (y\plus a \mult x_0)$ 
  12.179      by case analysis on $a$. \label{linorder_linear_split}*};
  12.180  
  12.181 -    also; have "... <= p (y + a <*> x0)";
  12.182 +    also; have "... <= p (y + a (*) x0)";
  12.183      proof (rule linorder_linear_split); 
  12.184  
  12.185        assume z: "a = 0r"; 
  12.186 @@ -284,27 +284,27 @@
  12.187      next;
  12.188        assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
  12.189        from a1; 
  12.190 -      have "- p (rinv a <*> y + x0) - h (rinv a <*> y) <= xi";
  12.191 +      have "- p (rinv a (*) y + x0) - h (rinv a (*) y) <= xi";
  12.192          by (rule bspec) (simp!);
  12.193  
  12.194        txt {* The thesis for this case now follows by a short  
  12.195        calculation. *};      
  12.196        hence "a * xi 
  12.197 -            <= a * (- p (rinv a <*> y + x0) - h (rinv a <*> y))";
  12.198 +            <= a * (- p (rinv a (*) y + x0) - h (rinv a (*) y))";
  12.199          by (rule real_mult_less_le_anti [OF lz]);
  12.200 -      also; have "... = - a * (p (rinv a <*> y + x0)) 
  12.201 -                        - a * (h (rinv a <*> y))";
  12.202 +      also; have "... = - a * (p (rinv a (*) y + x0)) 
  12.203 +                        - a * (h (rinv a (*) y))";
  12.204          by (rule real_mult_diff_distrib);
  12.205 -      also; from lz vs y; have "- a * (p (rinv a <*> y + x0)) 
  12.206 -                               = p (a <*> (rinv a <*> y + x0))";
  12.207 +      also; from lz vs y; have "- a * (p (rinv a (*) y + x0)) 
  12.208 +                               = p (a (*) (rinv a (*) y + x0))";
  12.209          by (simp add: seminorm_rabs_homogenous rabs_minus_eqI2);
  12.210 -      also; from nz vs y; have "... = p (y + a <*> x0)";
  12.211 +      also; from nz vs y; have "... = p (y + a (*) x0)";
  12.212          by (simp add: vs_add_mult_distrib1);
  12.213 -      also; from nz vs y; have "a * (h (rinv a <*> y)) =  h y";
  12.214 +      also; from nz vs y; have "a * (h (rinv a (*) y)) =  h y";
  12.215          by (simp add: linearform_mult [RS sym]);
  12.216 -      finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
  12.217 +      finally; have "a * xi <= p (y + a (*) x0) - h y"; .;
  12.218  
  12.219 -      hence "h y + a * xi <= h y + p (y + a <*> x0) - h y";
  12.220 +      hence "h y + a * xi <= h y + p (y + a (*) x0) - h y";
  12.221          by (simp add: real_add_left_cancel_le);
  12.222        thus ?thesis; by simp;
  12.223  
  12.224 @@ -314,30 +314,30 @@
  12.225      next; 
  12.226        assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
  12.227        from a2;
  12.228 -      have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
  12.229 +      have "xi <= p (rinv a (*) y + x0) - h (rinv a (*) y)";
  12.230          by (rule bspec) (simp!);
  12.231  
  12.232        txt {* The thesis for this case follows by a short
  12.233        calculation: *};
  12.234  
  12.235        with gz; have "a * xi 
  12.236 -            <= a * (p (rinv a <*> y + x0) - h (rinv a <*> y))";
  12.237 +            <= a * (p (rinv a (*) y + x0) - h (rinv a (*) y))";
  12.238          by (rule real_mult_less_le_mono);
  12.239 -      also; have "... = a * p (rinv a <*> y + x0) 
  12.240 -                        - a * h (rinv a <*> y)";
  12.241 +      also; have "... = a * p (rinv a (*) y + x0) 
  12.242 +                        - a * h (rinv a (*) y)";
  12.243          by (rule real_mult_diff_distrib2); 
  12.244        also; from gz vs y; 
  12.245 -      have "a * p (rinv a <*> y + x0) 
  12.246 -           = p (a <*> (rinv a <*> y + x0))";
  12.247 +      have "a * p (rinv a (*) y + x0) 
  12.248 +           = p (a (*) (rinv a (*) y + x0))";
  12.249          by (simp add: seminorm_rabs_homogenous rabs_eqI2);
  12.250        also; from nz vs y; 
  12.251 -      have "... = p (y + a <*> x0)";
  12.252 +      have "... = p (y + a (*) x0)";
  12.253          by (simp add: vs_add_mult_distrib1);
  12.254 -      also; from nz vs y; have "a * h (rinv a <*> y) = h y";
  12.255 +      also; from nz vs y; have "a * h (rinv a (*) y) = h y";
  12.256          by (simp add: linearform_mult [RS sym]); 
  12.257 -      finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
  12.258 +      finally; have "a * xi <= p (y + a (*) x0) - h y"; .;
  12.259   
  12.260 -      hence "h y + a * xi <= h y + (p (y + a <*> x0) - h y)";
  12.261 +      hence "h y + a * xi <= h y + (p (y + a (*) x0) - h y)";
  12.262          by (simp add: real_add_left_cancel_le);
  12.263        thus ?thesis; by simp;
  12.264      qed;
    13.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Apr 13 15:01:45 2000 +0200
    13.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Apr 13 15:01:50 2000 +0200
    13.3 @@ -437,16 +437,16 @@
    13.4  
    13.5      txt{* We have to show that $h$ is multiplicative. *};
    13.6  
    13.7 -    thus "h (a <*> x) = a * h x";
    13.8 +    thus "h (a (*) x) = a * h x";
    13.9      proof (elim exE conjE);
   13.10        fix H' h'; assume "x:H'"
   13.11          and b: "graph H' h' <= graph H h" 
   13.12          and "is_linearform H' h'" "is_subspace H' E";
   13.13 -      have "h' (a <*> x) = a * h' x"; 
   13.14 +      have "h' (a (*) x) = a * h' x"; 
   13.15          by (rule linearform_mult);
   13.16        also; have "h' x = h x"; ..;
   13.17 -      also; have "a <*> x : H'"; ..;
   13.18 -      with b; have "h' (a <*> x) = h (a <*> x)"; ..;
   13.19 +      also; have "a (*) x : H'"; ..;
   13.20 +      with b; have "h' (a (*) x) = h (a (*) x)"; ..;
   13.21        finally; show ?thesis; .;
   13.22      qed;
   13.23    qed;
   13.24 @@ -507,7 +507,7 @@
   13.25  
   13.26    show ?thesis; 
   13.27    proof;
   13.28 -    show "<0> : F"; ..;
   13.29 +    show "00 : F"; ..;
   13.30      show "F <= H"; 
   13.31      proof (rule graph_extD2);
   13.32        show "graph F f <= graph H h";
   13.33 @@ -518,10 +518,10 @@
   13.34        fix x y; assume "x:F" "y:F";
   13.35        show "x + y : F"; by (simp!);
   13.36      qed;
   13.37 -    show "ALL x:F. ALL a. a <*> x : F";
   13.38 +    show "ALL x:F. ALL a. a (*) x : F";
   13.39      proof (intro ballI allI);
   13.40        fix x a; assume "x:F";
   13.41 -      show "a <*> x : F"; by (simp!);
   13.42 +      show "a (*) x : F"; by (simp!);
   13.43      qed;
   13.44    qed;
   13.45  qed;
   13.46 @@ -542,10 +542,10 @@
   13.47      txt {* The $\zero$ element is in $H$, as $F$ is a subset 
   13.48      of $H$: *};
   13.49  
   13.50 -    have "<0> : F"; ..;
   13.51 +    have "00 : F"; ..;
   13.52      also; have "is_subspace F H"; by (rule sup_supF); 
   13.53      hence "F <= H"; ..;
   13.54 -    finally; show "<0> : H"; .;
   13.55 +    finally; show "00 : H"; .;
   13.56  
   13.57      txt{* $H$ is a subset of $E$: *};
   13.58  
   13.59 @@ -588,7 +588,7 @@
   13.60  
   13.61      txt{* $H$ is closed under scalar multiplication: *};
   13.62  
   13.63 -    show "ALL x:H. ALL a. a <*> x : H"; 
   13.64 +    show "ALL x:H. ALL a. a (*) x : H"; 
   13.65      proof (intro ballI allI); 
   13.66        fix x a; assume "x:H"; 
   13.67        have "EX H' h'. x:H' & graph H' h' <= graph H h
   13.68 @@ -596,11 +596,11 @@
   13.69                & is_subspace F H' & graph F f <= graph H' h' 
   13.70                & (ALL x:H'. h' x <= p x)"; 
   13.71  	by (rule some_H'h'); 
   13.72 -      thus "a <*> x : H"; 
   13.73 +      thus "a (*) x : H"; 
   13.74        proof (elim exE conjE);
   13.75  	fix H' h'; 
   13.76          assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
   13.77 -        have "a <*> x : H'"; ..;
   13.78 +        have "a (*) x : H'"; ..;
   13.79          also; have "H' <= H"; ..;
   13.80  	finally; show ?thesis; .;
   13.81        qed;
    14.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Thu Apr 13 15:01:45 2000 +0200
    14.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Thu Apr 13 15:01:50 2000 +0200
    14.3 @@ -14,11 +14,11 @@
    14.4    is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" 
    14.5    "is_linearform V f == 
    14.6        (ALL x: V. ALL y: V. f (x + y) = f x + f y) &
    14.7 -      (ALL x: V. ALL a. f (a <*> x) = a * (f x))"; 
    14.8 +      (ALL x: V. ALL a. f (a (*) x) = a * (f x))"; 
    14.9  
   14.10  lemma is_linearformI [intro]: 
   14.11    "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y;
   14.12 -    !! x c. x : V ==> f (c <*> x) = c * f x |]
   14.13 +    !! x c. x : V ==> f (c (*) x) = c * f x |]
   14.14   ==> is_linearform V f";
   14.15   by (unfold is_linearform_def) force;
   14.16  
   14.17 @@ -27,7 +27,7 @@
   14.18    by (unfold is_linearform_def) fast;
   14.19  
   14.20  lemma linearform_mult [intro??]: 
   14.21 -  "[| is_linearform V f; x:V |] ==>  f (a <*> x) = a * (f x)"; 
   14.22 +  "[| is_linearform V f; x:V |] ==>  f (a (*) x) = a * (f x)"; 
   14.23    by (unfold is_linearform_def) fast;
   14.24  
   14.25  lemma linearform_neg [intro??]:
   14.26 @@ -35,7 +35,7 @@
   14.27    ==> f (- x) = - f x";
   14.28  proof -; 
   14.29    assume "is_linearform V f" "is_vectorspace V" "x:V"; 
   14.30 -  have "f (- x) = f ((- 1r) <*> x)"; by (simp! add: negate_eq1);
   14.31 +  have "f (- x) = f ((- 1r) (*) x)"; by (simp! add: negate_eq1);
   14.32    also; have "... = (- 1r) * (f x)"; by (rule linearform_mult);
   14.33    also; have "... = - (f x)"; by (simp!);
   14.34    finally; show ?thesis; .;
   14.35 @@ -56,14 +56,14 @@
   14.36  text{* Every linear form yields $0$ for the $\zero$ vector.*};
   14.37  
   14.38  lemma linearform_zero [intro??, simp]: 
   14.39 -  "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
   14.40 +  "[| is_vectorspace V; is_linearform V f |] ==> f 00 = 0r"; 
   14.41  proof -; 
   14.42    assume "is_vectorspace V" "is_linearform V f";
   14.43 -  have "f <0> = f (<0> - <0>)"; by (simp!);
   14.44 -  also; have "... = f <0> - f <0>"; 
   14.45 +  have "f 00 = f (00 - 00)"; by (simp!);
   14.46 +  also; have "... = f 00 - f 00"; 
   14.47      by (rule linearform_diff) (simp!)+;
   14.48    also; have "... = 0r"; by simp;
   14.49 -  finally; show "f <0> = 0r"; .;
   14.50 +  finally; show "f 00 = 0r"; .;
   14.51  qed; 
   14.52  
   14.53  end;
   14.54 \ No newline at end of file
    15.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Apr 13 15:01:45 2000 +0200
    15.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Apr 13 15:01:50 2000 +0200
    15.3 @@ -19,12 +19,12 @@
    15.4    is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool"
    15.5    "is_seminorm V norm == ALL x: V. ALL y:V. ALL a. 
    15.6          0r <= norm x 
    15.7 -      & norm (a <*> x) = (rabs a) * (norm x)
    15.8 +      & norm (a (*) x) = (rabs a) * (norm x)
    15.9        & norm (x + y) <= norm x + norm y";
   15.10  
   15.11  lemma is_seminormI [intro]: 
   15.12    "[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x;
   15.13 -  !! x a. x:V ==> norm (a <*> x) = (rabs a) * (norm x);
   15.14 +  !! x a. x:V ==> norm (a (*) x) = (rabs a) * (norm x);
   15.15    !! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] 
   15.16    ==> is_seminorm V norm";
   15.17    by (unfold is_seminorm_def, force);
   15.18 @@ -35,7 +35,7 @@
   15.19  
   15.20  lemma seminorm_rabs_homogenous: 
   15.21    "[| is_seminorm V norm; x:V |] 
   15.22 -  ==> norm (a <*> x) = (rabs a) * (norm x)";
   15.23 +  ==> norm (a (*) x) = (rabs a) * (norm x)";
   15.24    by (unfold is_seminorm_def, force);
   15.25  
   15.26  lemma seminorm_subadditive: 
   15.27 @@ -48,11 +48,11 @@
   15.28    ==> norm (x - y) <= norm x + norm y";
   15.29  proof -;
   15.30    assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V";
   15.31 -  have "norm (x - y) = norm (x + - 1r <*> y)";  
   15.32 +  have "norm (x - y) = norm (x + - 1r (*) y)";  
   15.33      by (simp! add: diff_eq2 negate_eq2);
   15.34 -  also; have "... <= norm x + norm  (- 1r <*> y)"; 
   15.35 +  also; have "... <= norm x + norm  (- 1r (*) y)"; 
   15.36      by (simp! add: seminorm_subadditive);
   15.37 -  also; have "norm (- 1r <*> y) = rabs (- 1r) * norm y"; 
   15.38 +  also; have "norm (- 1r (*) y) = rabs (- 1r) * norm y"; 
   15.39      by (rule seminorm_rabs_homogenous);
   15.40    also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
   15.41    finally; show "norm (x - y) <= norm x + norm y"; by simp;
   15.42 @@ -63,7 +63,7 @@
   15.43    ==> norm (- x) = norm x";
   15.44  proof -;
   15.45    assume "is_seminorm V norm" "x:V" "is_vectorspace V";
   15.46 -  have "norm (- x) = norm (- 1r <*> x)"; by (simp! only: negate_eq1);
   15.47 +  have "norm (- x) = norm (- 1r (*) x)"; by (simp! only: negate_eq1);
   15.48    also; have "... = rabs (- 1r) * norm x"; 
   15.49      by (rule seminorm_rabs_homogenous);
   15.50    also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
   15.51 @@ -79,10 +79,10 @@
   15.52  constdefs
   15.53    is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
   15.54    "is_norm V norm == ALL x: V.  is_seminorm V norm 
   15.55 -      & (norm x = 0r) = (x = <0>)";
   15.56 +      & (norm x = 0r) = (x = 00)";
   15.57  
   15.58  lemma is_normI [intro]: 
   15.59 -  "ALL x: V.  is_seminorm V norm  & (norm x = 0r) = (x = <0>) 
   15.60 +  "ALL x: V.  is_seminorm V norm  & (norm x = 0r) = (x = 00) 
   15.61    ==> is_norm V norm"; by (simp only: is_norm_def);
   15.62  
   15.63  lemma norm_is_seminorm [intro??]: 
   15.64 @@ -90,7 +90,7 @@
   15.65    by (unfold is_norm_def, force);
   15.66  
   15.67  lemma norm_zero_iff: 
   15.68 -  "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)";
   15.69 +  "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = 00)";
   15.70    by (unfold is_norm_def, force);
   15.71  
   15.72  lemma norm_ge_zero [intro??]:
   15.73 @@ -128,15 +128,15 @@
   15.74    by (unfold is_normed_vectorspace_def, rule, elim conjE);
   15.75  
   15.76  lemma normed_vs_norm_gt_zero [intro??]: 
   15.77 -  "[| is_normed_vectorspace V norm; x:V; x ~= <0> |] ==> 0r < norm x";
   15.78 +  "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> 0r < norm x";
   15.79  proof (unfold is_normed_vectorspace_def, elim conjE);
   15.80 -  assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm";
   15.81 +  assume "x : V" "x ~= 00" "is_vectorspace V" "is_norm V norm";
   15.82    have "0r <= norm x"; ..;
   15.83    also; have "0r ~= norm x";
   15.84    proof;
   15.85      presume "norm x = 0r";
   15.86 -    also; have "?this = (x = <0>)"; by (rule norm_zero_iff);
   15.87 -    finally; have "x = <0>"; .;
   15.88 +    also; have "?this = (x = 00)"; by (rule norm_zero_iff);
   15.89 +    finally; have "x = 00"; .;
   15.90      thus "False"; by contradiction;
   15.91    qed (rule sym);
   15.92    finally; show "0r < norm x"; .;
   15.93 @@ -144,7 +144,7 @@
   15.94  
   15.95  lemma normed_vs_norm_rabs_homogenous [intro??]: 
   15.96    "[| is_normed_vectorspace V norm; x:V |] 
   15.97 -  ==> norm (a <*> x) = (rabs a) * (norm x)";
   15.98 +  ==> norm (a (*) x) = (rabs a) * (norm x)";
   15.99    by (rule seminorm_rabs_homogenous, rule norm_is_seminorm, 
  15.100        rule normed_vs_norm);
  15.101  
  15.102 @@ -170,13 +170,13 @@
  15.103      proof;
  15.104        fix x y a; presume "x : E";
  15.105        show "0r <= norm x"; ..;
  15.106 -      show "norm (a <*> x) = rabs a * norm x"; ..;
  15.107 +      show "norm (a (*) x) = rabs a * norm x"; ..;
  15.108        presume "y : E";
  15.109        show "norm (x + y) <= norm x + norm y"; ..;
  15.110      qed (simp!)+;
  15.111  
  15.112      fix x; assume "x : F";
  15.113 -    show "(norm x = 0r) = (x = <0>)"; 
  15.114 +    show "(norm x = 0r) = (x = 00)"; 
  15.115      proof (rule norm_zero_iff);
  15.116        show "is_norm E norm"; ..;
  15.117      qed (simp!);
    16.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Thu Apr 13 15:01:45 2000 +0200
    16.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Apr 13 15:01:50 2000 +0200
    16.3 @@ -18,14 +18,14 @@
    16.4  constdefs 
    16.5    is_subspace ::  "['a::{minus, plus} set, 'a set] => bool"
    16.6    "is_subspace U V == U ~= {} & U <= V 
    16.7 -     & (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
    16.8 +     & (ALL x:U. ALL y:U. ALL a. x + y : U & a (*) x : U)";
    16.9  
   16.10  lemma subspaceI [intro]: 
   16.11 -  "[| <0> : U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
   16.12 -  ALL x:U. ALL a. a <*> x : U |]
   16.13 +  "[| 00 : U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
   16.14 +  ALL x:U. ALL a. a (*) x : U |]
   16.15    ==> is_subspace U V";
   16.16  proof (unfold is_subspace_def, intro conjI); 
   16.17 -  assume "<0> : U"; thus "U ~= {}"; by fast;
   16.18 +  assume "00 : U"; thus "U ~= {}"; by fast;
   16.19  qed (simp+);
   16.20  
   16.21  lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}";
   16.22 @@ -43,7 +43,7 @@
   16.23    by (unfold is_subspace_def) simp;
   16.24  
   16.25  lemma subspace_mult_closed [simp, intro??]: 
   16.26 -  "[| is_subspace U V; x:U |] ==> a <*> x : U";
   16.27 +  "[| is_subspace U V; x:U |] ==> a (*) x : U";
   16.28    by (unfold is_subspace_def) simp;
   16.29  
   16.30  lemma subspace_diff_closed [simp, intro??]: 
   16.31 @@ -56,7 +56,7 @@
   16.32  of the carrier set and by vector space laws.*};
   16.33  
   16.34  lemma zero_in_subspace [intro??]:
   16.35 -  "[| is_subspace U V; is_vectorspace V |] ==> <0> : U";
   16.36 +  "[| is_subspace U V; is_vectorspace V |] ==> 00 : U";
   16.37  proof -; 
   16.38    assume "is_subspace U V" and v: "is_vectorspace V";
   16.39    have "U ~= {}"; ..;
   16.40 @@ -65,7 +65,7 @@
   16.41    proof; 
   16.42      fix x; assume u: "x:U"; 
   16.43      hence "x:V"; by (simp!);
   16.44 -    with v; have "<0> = x - x"; by (simp!);
   16.45 +    with v; have "00 = x - x"; by (simp!);
   16.46      also; have "... : U"; by (rule subspace_diff_closed);
   16.47      finally; show ?thesis; .;
   16.48    qed;
   16.49 @@ -84,10 +84,10 @@
   16.50    assume "is_subspace U V" "is_vectorspace V";
   16.51    show ?thesis;
   16.52    proof; 
   16.53 -    show "<0> : U"; ..;
   16.54 -    show "ALL x:U. ALL a. a <*> x : U"; by (simp!);
   16.55 +    show "00 : U"; ..;
   16.56 +    show "ALL x:U. ALL a. a (*) x : U"; by (simp!);
   16.57      show "ALL x:U. ALL y:U. x + y : U"; by (simp!);
   16.58 -    show "ALL x:U. - x = -1r <*> x"; by (simp! add: negate_eq1);
   16.59 +    show "ALL x:U. - x = -1r (*) x"; by (simp! add: negate_eq1);
   16.60      show "ALL x:U. ALL y:U. x - y =  x + - y"; 
   16.61        by (simp! add: diff_eq1);
   16.62    qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
   16.63 @@ -98,10 +98,10 @@
   16.64  lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V";
   16.65  proof; 
   16.66    assume "is_vectorspace V";
   16.67 -  show "<0> : V"; ..;
   16.68 +  show "00 : V"; ..;
   16.69    show "V <= V"; ..;
   16.70    show "ALL x:V. ALL y:V. x + y : V"; by (simp!);
   16.71 -  show "ALL x:V. ALL a. a <*> x : V"; by (simp!);
   16.72 +  show "ALL x:V. ALL a. a (*) x : V"; by (simp!);
   16.73  qed;
   16.74  
   16.75  text {* The subspace relation is transitive. *};
   16.76 @@ -111,7 +111,7 @@
   16.77    ==> is_subspace U W";
   16.78  proof; 
   16.79    assume "is_subspace U V" "is_subspace V W" "is_vectorspace V";
   16.80 -  show "<0> : U"; ..;
   16.81 +  show "00 : U"; ..;
   16.82  
   16.83    have "U <= V"; ..;
   16.84    also; have "V <= W"; ..;
   16.85 @@ -123,10 +123,10 @@
   16.86      show "x + y : U"; by (simp!);
   16.87    qed;
   16.88  
   16.89 -  show "ALL x:U. ALL a. a <*> x : U";
   16.90 +  show "ALL x:U. ALL a. a (*) x : U";
   16.91    proof (intro ballI allI);
   16.92      fix x a; assume "x:U";
   16.93 -    show "a <*> x : U"; by (simp!);
   16.94 +    show "a (*) x : U"; by (simp!);
   16.95    qed;
   16.96  qed;
   16.97  
   16.98 @@ -139,12 +139,12 @@
   16.99  
  16.100  constdefs
  16.101    lin :: "'a => 'a set"
  16.102 -  "lin x == {a <*> x | a. True}"; 
  16.103 +  "lin x == {a (*) x | a. True}"; 
  16.104  
  16.105 -lemma linD: "x : lin v = (EX a::real. x = a <*> v)";
  16.106 +lemma linD: "x : lin v = (EX a::real. x = a (*) v)";
  16.107    by (unfold lin_def) fast;
  16.108  
  16.109 -lemma linI [intro??]: "a <*> x0 : lin x0";
  16.110 +lemma linI [intro??]: "a (*) x0 : lin x0";
  16.111    by (unfold lin_def) fast;
  16.112  
  16.113  text {* Every vector is contained in its linear closure. *};
  16.114 @@ -152,7 +152,7 @@
  16.115  lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x";
  16.116  proof (unfold lin_def, intro CollectI exI conjI);
  16.117    assume "is_vectorspace V" "x:V";
  16.118 -  show "x = 1r <*> x"; by (simp!);
  16.119 +  show "x = 1r (*) x"; by (simp!);
  16.120  qed simp;
  16.121  
  16.122  text {* Any linear closure is a subspace. *};
  16.123 @@ -161,14 +161,14 @@
  16.124    "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
  16.125  proof;
  16.126    assume "is_vectorspace V" "x:V";
  16.127 -  show "<0> : lin x"; 
  16.128 +  show "00 : lin x"; 
  16.129    proof (unfold lin_def, intro CollectI exI conjI);
  16.130 -    show "<0> = 0r <*> x"; by (simp!);
  16.131 +    show "00 = 0r (*) x"; by (simp!);
  16.132    qed simp;
  16.133  
  16.134    show "lin x <= V";
  16.135    proof (unfold lin_def, intro subsetI, elim CollectE exE conjE); 
  16.136 -    fix xa a; assume "xa = a <*> x"; 
  16.137 +    fix xa a; assume "xa = a (*) x"; 
  16.138      show "xa:V"; by (simp!);
  16.139    qed;
  16.140  
  16.141 @@ -178,20 +178,20 @@
  16.142      thus "x1 + x2 : lin x";
  16.143      proof (unfold lin_def, elim CollectE exE conjE, 
  16.144        intro CollectI exI conjI);
  16.145 -      fix a1 a2; assume "x1 = a1 <*> x" "x2 = a2 <*> x";
  16.146 -      show "x1 + x2 = (a1 + a2) <*> x"; 
  16.147 +      fix a1 a2; assume "x1 = a1 (*) x" "x2 = a2 (*) x";
  16.148 +      show "x1 + x2 = (a1 + a2) (*) x"; 
  16.149          by (simp! add: vs_add_mult_distrib2);
  16.150      qed simp;
  16.151    qed;
  16.152  
  16.153 -  show "ALL xa:lin x. ALL a. a <*> xa : lin x"; 
  16.154 +  show "ALL xa:lin x. ALL a. a (*) xa : lin x"; 
  16.155    proof (intro ballI allI);
  16.156      fix x1 a; assume "x1 : lin x"; 
  16.157 -    thus "a <*> x1 : lin x";
  16.158 +    thus "a (*) x1 : lin x";
  16.159      proof (unfold lin_def, elim CollectE exE conjE,
  16.160        intro CollectI exI conjI);
  16.161 -      fix a1; assume "x1 = a1 <*> x";
  16.162 -      show "a <*> x1 = (a * a1) <*> x"; by (simp!);
  16.163 +      fix a1; assume "x1 = a1 (*) x";
  16.164 +      show "a (*) x1 = (a * a1) (*) x"; by (simp!);
  16.165      qed simp;
  16.166    qed; 
  16.167  qed;
  16.168 @@ -240,20 +240,20 @@
  16.169    ==> is_subspace U (U + V)";
  16.170  proof; 
  16.171    assume "is_vectorspace U" "is_vectorspace V";
  16.172 -  show "<0> : U"; ..;
  16.173 +  show "00 : U"; ..;
  16.174    show "U <= U + V";
  16.175    proof (intro subsetI vs_sumI);
  16.176    fix x; assume "x:U";
  16.177 -    show "x = x + <0>"; by (simp!);
  16.178 -    show "<0> : V"; by (simp!);
  16.179 +    show "x = x + 00"; by (simp!);
  16.180 +    show "00 : V"; by (simp!);
  16.181    qed;
  16.182    show "ALL x:U. ALL y:U. x + y : U"; 
  16.183    proof (intro ballI);
  16.184      fix x y; assume "x:U" "y:U"; show "x + y : U"; by (simp!);
  16.185    qed;
  16.186 -  show "ALL x:U. ALL a. a <*> x : U"; 
  16.187 +  show "ALL x:U. ALL a. a (*) x : U"; 
  16.188    proof (intro ballI allI);
  16.189 -    fix x a; assume "x:U"; show "a <*> x : U"; by (simp!);
  16.190 +    fix x a; assume "x:U"; show "a (*) x : U"; by (simp!);
  16.191    qed;
  16.192  qed;
  16.193  
  16.194 @@ -264,11 +264,11 @@
  16.195    ==> is_subspace (U + V) E";
  16.196  proof; 
  16.197    assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
  16.198 -  show "<0> : U + V";
  16.199 +  show "00 : U + V";
  16.200    proof (intro vs_sumI);
  16.201 -    show "<0> : U"; ..;
  16.202 -    show "<0> : V"; ..;
  16.203 -    show "(<0>::'a) = <0> + <0>"; by (simp!);
  16.204 +    show "00 : U"; ..;
  16.205 +    show "00 : V"; ..;
  16.206 +    show "(00::'a) = 00 + 00"; by (simp!);
  16.207    qed;
  16.208    
  16.209    show "U + V <= E";
  16.210 @@ -289,13 +289,13 @@
  16.211      qed (simp!)+;
  16.212    qed;
  16.213  
  16.214 -  show "ALL x : U + V. ALL a. a <*> x : U + V";
  16.215 +  show "ALL x : U + V. ALL a. a (*) x : U + V";
  16.216    proof (intro ballI allI);
  16.217      fix x a; assume "x : U + V";
  16.218 -    thus "a <*> x : U + V";
  16.219 +    thus "a (*) x : U + V";
  16.220      proof (elim vs_sumE bexE, intro vs_sumI);
  16.221        fix a x u v; assume "u : U" "v : V" "x = u + v";
  16.222 -      show "a <*> x = (a <*> u) + (a <*> v)"; 
  16.223 +      show "a (*) x = (a (*) u) + (a (*) v)"; 
  16.224          by (simp! add: vs_add_mult_distrib1);
  16.225      qed (simp!)+;
  16.226    qed;
  16.227 @@ -323,11 +323,11 @@
  16.228  
  16.229  lemma decomp: 
  16.230    "[| is_vectorspace E; is_subspace U E; is_subspace V E; 
  16.231 -  U Int V = {<0>}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |] 
  16.232 +  U Int V = {00}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |] 
  16.233    ==> u1 = u2 & v1 = v2"; 
  16.234  proof; 
  16.235    assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"  
  16.236 -    "U Int V = {<0>}" "u1:U" "u2:U" "v1:V" "v2:V" 
  16.237 +    "U Int V = {00}" "u1:U" "u2:U" "v1:V" "v2:V" 
  16.238      "u1 + v1 = u2 + v2"; 
  16.239    have eq: "u1 - u2 = v2 - v1"; by (simp! add: vs_add_diff_swap);
  16.240    have u: "u1 - u2 : U"; by (simp!); 
  16.241 @@ -337,14 +337,14 @@
  16.242    
  16.243    show "u1 = u2";
  16.244    proof (rule vs_add_minus_eq);
  16.245 -    show "u1 - u2 = <0>"; by (rule Int_singletonD [OF _ u u']); 
  16.246 +    show "u1 - u2 = 00"; by (rule Int_singletonD [OF _ u u']); 
  16.247      show "u1 : E"; ..;
  16.248      show "u2 : E"; ..;
  16.249    qed;
  16.250  
  16.251    show "v1 = v2";
  16.252    proof (rule vs_add_minus_eq [RS sym]);
  16.253 -    show "v2 - v1 = <0>"; by (rule Int_singletonD [OF _ v' v]);
  16.254 +    show "v2 - v1 = 00"; by (rule Int_singletonD [OF _ v' v]);
  16.255      show "v1 : E"; ..;
  16.256      show "v2 : E"; ..;
  16.257    qed;
  16.258 @@ -358,44 +358,44 @@
  16.259  
  16.260  lemma decomp_H0: 
  16.261    "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 
  16.262 -  x0 ~: H; x0 : E; x0 ~= <0>; y1 + a1 <*> x0 = y2 + a2 <*> x0 |]
  16.263 +  x0 ~: H; x0 : E; x0 ~= 00; y1 + a1 (*) x0 = y2 + a2 (*) x0 |]
  16.264    ==> y1 = y2 & a1 = a2";
  16.265  proof;
  16.266    assume "is_vectorspace E" and h: "is_subspace H E"
  16.267 -     and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
  16.268 -         "y1 + a1 <*> x0 = y2 + a2 <*> x0";
  16.269 +     and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= 00" 
  16.270 +         "y1 + a1 (*) x0 = y2 + a2 (*) x0";
  16.271  
  16.272 -  have c: "y1 = y2 & a1 <*> x0 = a2 <*> x0";
  16.273 +  have c: "y1 = y2 & a1 (*) x0 = a2 (*) x0";
  16.274    proof (rule decomp); 
  16.275 -    show "a1 <*> x0 : lin x0"; ..; 
  16.276 -    show "a2 <*> x0 : lin x0"; ..;
  16.277 -    show "H Int (lin x0) = {<0>}"; 
  16.278 +    show "a1 (*) x0 : lin x0"; ..; 
  16.279 +    show "a2 (*) x0 : lin x0"; ..;
  16.280 +    show "H Int (lin x0) = {00}"; 
  16.281      proof;
  16.282 -      show "H Int lin x0 <= {<0>}"; 
  16.283 +      show "H Int lin x0 <= {00}"; 
  16.284        proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
  16.285          fix x; assume "x:H" "x : lin x0"; 
  16.286 -        thus "x = <0>";
  16.287 +        thus "x = 00";
  16.288          proof (unfold lin_def, elim CollectE exE conjE);
  16.289 -          fix a; assume "x = a <*> x0";
  16.290 +          fix a; assume "x = a (*) x0";
  16.291            show ?thesis;
  16.292            proof cases;
  16.293              assume "a = 0r"; show ?thesis; by (simp!);
  16.294            next;
  16.295              assume "a ~= 0r"; 
  16.296 -            from h; have "rinv a <*> a <*> x0 : H"; 
  16.297 +            from h; have "rinv a (*) a (*) x0 : H"; 
  16.298                by (rule subspace_mult_closed) (simp!);
  16.299 -            also; have "rinv a <*> a <*> x0 = x0"; by (simp!);
  16.300 +            also; have "rinv a (*) a (*) x0 = x0"; by (simp!);
  16.301              finally; have "x0 : H"; .;
  16.302              thus ?thesis; by contradiction;
  16.303            qed;
  16.304         qed;
  16.305        qed;
  16.306 -      show "{<0>} <= H Int lin x0";
  16.307 +      show "{00} <= H Int lin x0";
  16.308        proof -;
  16.309 -	have "<0>: H Int lin x0";
  16.310 +	have "00: H Int lin x0";
  16.311  	proof (rule IntI);
  16.312 -	  show "<0>:H"; ..;
  16.313 -	  from lin_vs; show "<0> : lin x0"; ..;
  16.314 +	  show "00:H"; ..;
  16.315 +	  from lin_vs; show "00 : lin x0"; ..;
  16.316  	qed;
  16.317  	thus ?thesis; by simp;
  16.318        qed;
  16.319 @@ -407,7 +407,7 @@
  16.320    
  16.321    show  "a1 = a2"; 
  16.322    proof (rule vs_mult_right_cancel [RS iffD1]);
  16.323 -    from c; show "a1 <*> x0 = a2 <*> x0"; by simp;
  16.324 +    from c; show "a1 (*) x0 = a2 (*) x0"; by simp;
  16.325    qed;
  16.326  qed;
  16.327  
  16.328 @@ -418,13 +418,13 @@
  16.329  
  16.330  lemma decomp_H0_H: 
  16.331    "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
  16.332 -  x0 ~= <0> |] 
  16.333 -  ==> (SOME (y, a). t = y + a <*> x0 & y : H) = (t, 0r)";
  16.334 +  x0 ~= 00 |] 
  16.335 +  ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, 0r)";
  16.336  proof (rule, unfold split_paired_all);
  16.337    assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
  16.338 -    "x0 ~= <0>";
  16.339 +    "x0 ~= 00";
  16.340    have h: "is_vectorspace H"; ..;
  16.341 -  fix y a; presume t1: "t = y + a <*> x0" and "y:H";
  16.342 +  fix y a; presume t1: "t = y + a (*) x0" and "y:H";
  16.343    have "y = t & a = 0r"; 
  16.344      by (rule decomp_H0) (assumption | (simp!))+;
  16.345    thus "(y, a) = (t, 0r)"; by (simp!);
  16.346 @@ -435,40 +435,40 @@
  16.347  $h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
  16.348  
  16.349  lemma h0_definite:
  16.350 -  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
  16.351 +  "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H)
  16.352                  in (h y) + a * xi);
  16.353 -  x = y + a <*> x0; is_vectorspace E; is_subspace H E;
  16.354 -  y:H; x0 ~: H; x0:E; x0 ~= <0> |]
  16.355 +  x = y + a (*) x0; is_vectorspace E; is_subspace H E;
  16.356 +  y:H; x0 ~: H; x0:E; x0 ~= 00 |]
  16.357    ==> h0 x = h y + a * xi";
  16.358  proof -;  
  16.359    assume 
  16.360 -    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
  16.361 +    "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H)
  16.362                 in (h y) + a * xi)"
  16.363 -    "x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
  16.364 -    "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
  16.365 +    "x = y + a (*) x0" "is_vectorspace E" "is_subspace H E"
  16.366 +    "y:H" "x0 ~: H" "x0:E" "x0 ~= 00";
  16.367    have "x : H + (lin x0)"; 
  16.368      by (simp! add: vs_sum_def lin_def) force+;
  16.369 -  have "EX! xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)"; 
  16.370 +  have "EX! xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)"; 
  16.371    proof;
  16.372 -    show "EX xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
  16.373 +    show "EX xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)";
  16.374        by (force!);
  16.375    next;
  16.376      fix xa ya;
  16.377 -    assume "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
  16.378 -           "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
  16.379 +    assume "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) xa"
  16.380 +           "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) ya";
  16.381      show "xa = ya"; ;
  16.382      proof -;
  16.383        show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
  16.384          by (rule Pair_fst_snd_eq [RS iffD2]);
  16.385 -      have x: "x = fst xa + snd xa <*> x0 & fst xa : H"; 
  16.386 +      have x: "x = fst xa + snd xa (*) x0 & fst xa : H"; 
  16.387          by (force!);
  16.388 -      have y: "x = fst ya + snd ya <*> x0 & fst ya : H"; 
  16.389 +      have y: "x = fst ya + snd ya (*) x0 & fst ya : H"; 
  16.390          by (force!);
  16.391        from x y; show "fst xa = fst ya & snd xa = snd ya"; 
  16.392          by (elim conjE) (rule decomp_H0, (simp!)+);
  16.393      qed;
  16.394    qed;
  16.395 -  hence eq: "(SOME (y, a). x = y + a <*> x0 & y:H) = (y, a)"; 
  16.396 +  hence eq: "(SOME (y, a). x = y + a (*) x0 & y:H) = (y, a)"; 
  16.397      by (rule select1_equality) (force!);
  16.398    thus "h0 x = h y + a * xi"; by (simp! add: Let_def);
  16.399  qed;
    17.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Apr 13 15:01:45 2000 +0200
    17.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Thu Apr 13 15:01:50 2000 +0200
    17.3 @@ -15,8 +15,8 @@
    17.4  element $\zero$ is defined. *};
    17.5  
    17.6  consts
    17.7 -  prod  :: "[real, 'a] => 'a"                       (infixr "<*>" 70)
    17.8 -  zero  :: 'a                                       ("<0>");
    17.9 +  prod  :: "[real, 'a] => 'a"                       (infixr "'(*')" 70)
   17.10 +  zero  :: 'a                                       ("00");
   17.11  
   17.12  syntax (symbols)
   17.13    prod  :: "[real, 'a] => 'a"                       (infixr "\<prod>" 70)
   17.14 @@ -29,7 +29,7 @@
   17.15  (***
   17.16  constdefs 
   17.17    negate :: "'a => 'a"                           ("- _" [100] 100)
   17.18 -  "- x == (- 1r) <*> x"
   17.19 +  "- x == (- 1r) ( * ) x"
   17.20    diff :: "'a => 'a => 'a"                       (infixl "-" 68)
   17.21    "x - y == x + - y";
   17.22  ***)
   17.23 @@ -51,34 +51,34 @@
   17.24    "is_vectorspace V == V ~= {} 
   17.25     & (ALL x:V. ALL y:V. ALL z:V. ALL a b.
   17.26          x + y : V                                 
   17.27 -      & a <*> x : V                                 
   17.28 +      & a (*) x : V                                 
   17.29        & (x + y) + z = x + (y + z)             
   17.30        & x + y = y + x                           
   17.31 -      & x - x = <0>                               
   17.32 -      & <0> + x = x                               
   17.33 -      & a <*> (x + y) = a <*> x + a <*> y       
   17.34 -      & (a + b) <*> x = a <*> x + b <*> x         
   17.35 -      & (a * b) <*> x = a <*> b <*> x               
   17.36 -      & 1r <*> x = x
   17.37 -      & - x = (- 1r) <*> x
   17.38 +      & x - x = 00                               
   17.39 +      & 00 + x = x                               
   17.40 +      & a (*) (x + y) = a (*) x + a (*) y       
   17.41 +      & (a + b) (*) x = a (*) x + b (*) x         
   17.42 +      & (a * b) (*) x = a (*) b (*) x               
   17.43 +      & 1r (*) x = x
   17.44 +      & - x = (- 1r) (*) x
   17.45        & x - y = x + - y)";                             
   17.46  
   17.47  text_raw {* \medskip *};
   17.48  text {* The corresponding introduction rule is:*};
   17.49  
   17.50  lemma vsI [intro]:
   17.51 -  "[| <0>:V; 
   17.52 +  "[| 00:V; 
   17.53    ALL x:V. ALL y:V. x + y : V; 
   17.54 -  ALL x:V. ALL a. a <*> x : V;  
   17.55 +  ALL x:V. ALL a. a (*) x : V;  
   17.56    ALL x:V. ALL y:V. ALL z:V. (x + y) + z = x + (y + z);
   17.57    ALL x:V. ALL y:V. x + y = y + x;
   17.58 -  ALL x:V. x - x = <0>;
   17.59 -  ALL x:V. <0> + x = x;
   17.60 -  ALL x:V. ALL y:V. ALL a. a <*> (x + y) = a <*> x + a <*> y;
   17.61 -  ALL x:V. ALL a b. (a + b) <*> x = a <*> x + b <*> x;
   17.62 -  ALL x:V. ALL a b. (a * b) <*> x = a <*> b <*> x; 
   17.63 -  ALL x:V. 1r <*> x = x; 
   17.64 -  ALL x:V. - x = (- 1r) <*> x; 
   17.65 +  ALL x:V. x - x = 00;
   17.66 +  ALL x:V. 00 + x = x;
   17.67 +  ALL x:V. ALL y:V. ALL a. a (*) (x + y) = a (*) x + a (*) y;
   17.68 +  ALL x:V. ALL a b. (a + b) (*) x = a (*) x + b (*) x;
   17.69 +  ALL x:V. ALL a b. (a * b) (*) x = a (*) b (*) x; 
   17.70 +  ALL x:V. 1r (*) x = x; 
   17.71 +  ALL x:V. - x = (- 1r) (*) x; 
   17.72    ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V";
   17.73  proof (unfold is_vectorspace_def, intro conjI ballI allI);
   17.74    fix x y z; 
   17.75 @@ -91,7 +91,7 @@
   17.76  text {* The corresponding destruction rules are: *};
   17.77  
   17.78  lemma negate_eq1: 
   17.79 -  "[| is_vectorspace V; x:V |] ==> - x = (- 1r) <*> x";
   17.80 +  "[| is_vectorspace V; x:V |] ==> - x = (- 1r) (*) x";
   17.81    by (unfold is_vectorspace_def) simp;
   17.82  
   17.83  lemma diff_eq1: 
   17.84 @@ -99,7 +99,7 @@
   17.85    by (unfold is_vectorspace_def) simp; 
   17.86  
   17.87  lemma negate_eq2: 
   17.88 -  "[| is_vectorspace V; x:V |] ==> (- 1r) <*> x = - x";
   17.89 +  "[| is_vectorspace V; x:V |] ==> (- 1r) (*) x = - x";
   17.90    by (unfold is_vectorspace_def) simp;
   17.91  
   17.92  lemma diff_eq2: 
   17.93 @@ -114,7 +114,7 @@
   17.94    by (unfold is_vectorspace_def) simp;
   17.95  
   17.96  lemma vs_mult_closed [simp, intro??]: 
   17.97 -  "[| is_vectorspace V; x:V |] ==> a <*> x : V"; 
   17.98 +  "[| is_vectorspace V; x:V |] ==> a (*) x : V"; 
   17.99    by (unfold is_vectorspace_def) simp;
  17.100  
  17.101  lemma vs_diff_closed [simp, intro??]: 
  17.102 @@ -149,13 +149,13 @@
  17.103  theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute;
  17.104  
  17.105  lemma vs_diff_self [simp]: 
  17.106 -  "[| is_vectorspace V; x:V |] ==>  x - x = <0>"; 
  17.107 +  "[| is_vectorspace V; x:V |] ==>  x - x = 00"; 
  17.108    by (unfold is_vectorspace_def) simp;
  17.109  
  17.110  text {* The existence of the zero element of a vector space
  17.111  follows from the non-emptiness of carrier set. *};
  17.112  
  17.113 -lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
  17.114 +lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 00:V";
  17.115  proof -; 
  17.116    assume "is_vectorspace V";
  17.117    have "V ~= {}"; ..;
  17.118 @@ -163,64 +163,64 @@
  17.119    thus ?thesis; 
  17.120    proof; 
  17.121      fix x; assume "x:V"; 
  17.122 -    have "<0> = x - x"; by (simp!);
  17.123 +    have "00 = x - x"; by (simp!);
  17.124      also; have "... : V"; by (simp! only: vs_diff_closed);
  17.125      finally; show ?thesis; .;
  17.126    qed;
  17.127  qed;
  17.128  
  17.129  lemma vs_add_zero_left [simp]: 
  17.130 -  "[| is_vectorspace V; x:V |] ==>  <0> + x = x";
  17.131 +  "[| is_vectorspace V; x:V |] ==>  00 + x = x";
  17.132    by (unfold is_vectorspace_def) simp;
  17.133  
  17.134  lemma vs_add_zero_right [simp]: 
  17.135 -  "[| is_vectorspace V; x:V |] ==>  x + <0> = x";
  17.136 +  "[| is_vectorspace V; x:V |] ==>  x + 00 = x";
  17.137  proof -;
  17.138    assume "is_vectorspace V" "x:V";
  17.139 -  hence "x + <0> = <0> + x"; by simp;
  17.140 +  hence "x + 00 = 00 + x"; by simp;
  17.141    also; have "... = x"; by (simp!);
  17.142    finally; show ?thesis; .;
  17.143  qed;
  17.144  
  17.145  lemma vs_add_mult_distrib1: 
  17.146    "[| is_vectorspace V; x:V; y:V |] 
  17.147 -  ==> a <*> (x + y) = a <*> x + a <*> y";
  17.148 +  ==> a (*) (x + y) = a (*) x + a (*) y";
  17.149    by (unfold is_vectorspace_def) simp;
  17.150  
  17.151  lemma vs_add_mult_distrib2: 
  17.152    "[| is_vectorspace V; x:V |] 
  17.153 -  ==> (a + b) <*> x = a <*> x + b <*> x"; 
  17.154 +  ==> (a + b) (*) x = a (*) x + b (*) x"; 
  17.155    by (unfold is_vectorspace_def) simp;
  17.156  
  17.157  lemma vs_mult_assoc: 
  17.158 -  "[| is_vectorspace V; x:V |] ==> (a * b) <*> x = a <*> (b <*> x)";
  17.159 +  "[| is_vectorspace V; x:V |] ==> (a * b) (*) x = a (*) (b (*) x)";
  17.160    by (unfold is_vectorspace_def) simp;
  17.161  
  17.162  lemma vs_mult_assoc2 [simp]: 
  17.163 - "[| is_vectorspace V; x:V |] ==> a <*> b <*> x = (a * b) <*> x";
  17.164 + "[| is_vectorspace V; x:V |] ==> a (*) b (*) x = (a * b) (*) x";
  17.165    by (simp only: vs_mult_assoc);
  17.166  
  17.167  lemma vs_mult_1 [simp]: 
  17.168 -  "[| is_vectorspace V; x:V |] ==> 1r <*> x = x"; 
  17.169 +  "[| is_vectorspace V; x:V |] ==> 1r (*) x = x"; 
  17.170    by (unfold is_vectorspace_def) simp;
  17.171  
  17.172  lemma vs_diff_mult_distrib1: 
  17.173    "[| is_vectorspace V; x:V; y:V |] 
  17.174 -  ==> a <*> (x - y) = a <*> x - a <*> y";
  17.175 +  ==> a (*) (x - y) = a (*) x - a (*) y";
  17.176    by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1);
  17.177  
  17.178  lemma vs_diff_mult_distrib2: 
  17.179    "[| is_vectorspace V; x:V |] 
  17.180 -  ==> (a - b) <*> x = a <*> x - (b <*> x)";
  17.181 +  ==> (a - b) (*) x = a (*) x - (b (*) x)";
  17.182  proof -;
  17.183    assume "is_vectorspace V" "x:V";
  17.184 -  have " (a - b) <*> x = (a + - b ) <*> x"; 
  17.185 +  have " (a - b) (*) x = (a + - b ) (*) x"; 
  17.186      by (unfold real_diff_def, simp);
  17.187 -  also; have "... = a <*> x + (- b) <*> x"; 
  17.188 +  also; have "... = a (*) x + (- b) (*) x"; 
  17.189      by (rule vs_add_mult_distrib2);
  17.190 -  also; have "... = a <*> x + - (b <*> x)"; 
  17.191 +  also; have "... = a (*) x + - (b (*) x)"; 
  17.192      by (simp! add: negate_eq1);
  17.193 -  also; have "... = a <*> x - (b <*> x)"; 
  17.194 +  also; have "... = a (*) x - (b (*) x)"; 
  17.195      by (simp! add: diff_eq1);
  17.196    finally; show ?thesis; .;
  17.197  qed;
  17.198 @@ -230,34 +230,34 @@
  17.199  text{* Further derived laws: *};
  17.200  
  17.201  lemma vs_mult_zero_left [simp]: 
  17.202 -  "[| is_vectorspace V; x:V |] ==> 0r <*> x = <0>";
  17.203 +  "[| is_vectorspace V; x:V |] ==> 0r (*) x = 00";
  17.204  proof -;
  17.205    assume "is_vectorspace V" "x:V";
  17.206 -  have  "0r <*> x = (1r - 1r) <*> x"; by (simp only: real_diff_self);
  17.207 -  also; have "... = (1r + - 1r) <*> x"; by simp;
  17.208 -  also; have "... =  1r <*> x + (- 1r) <*> x"; 
  17.209 +  have  "0r (*) x = (1r - 1r) (*) x"; by (simp only: real_diff_self);
  17.210 +  also; have "... = (1r + - 1r) (*) x"; by simp;
  17.211 +  also; have "... =  1r (*) x + (- 1r) (*) x"; 
  17.212      by (rule vs_add_mult_distrib2);
  17.213 -  also; have "... = x + (- 1r) <*> x"; by (simp!);
  17.214 +  also; have "... = x + (- 1r) (*) x"; by (simp!);
  17.215    also; have "... = x + - x"; by (simp! add: negate_eq2);;
  17.216    also; have "... = x - x"; by (simp! add: diff_eq2);
  17.217 -  also; have "... = <0>"; by (simp!);
  17.218 +  also; have "... = 00"; by (simp!);
  17.219    finally; show ?thesis; .;
  17.220  qed;
  17.221  
  17.222  lemma vs_mult_zero_right [simp]: 
  17.223    "[| is_vectorspace (V:: 'a::{plus, minus} set) |] 
  17.224 -  ==> a <*> <0> = (<0>::'a)";
  17.225 +  ==> a (*) 00 = (00::'a)";
  17.226  proof -;
  17.227    assume "is_vectorspace V";
  17.228 -  have "a <*> <0> = a <*> (<0> - (<0>::'a))"; by (simp!);
  17.229 -  also; have "... =  a <*> <0> - a <*> <0>";
  17.230 +  have "a (*) 00 = a (*) (00 - (00::'a))"; by (simp!);
  17.231 +  also; have "... =  a (*) 00 - a (*) 00";
  17.232       by (rule vs_diff_mult_distrib1) (simp!)+;
  17.233 -  also; have "... = <0>"; by (simp!);
  17.234 +  also; have "... = 00"; by (simp!);
  17.235    finally; show ?thesis; .;
  17.236  qed;
  17.237  
  17.238  lemma vs_minus_mult_cancel [simp]:  
  17.239 -  "[| is_vectorspace V; x:V |] ==> (- a) <*> - x = a <*> x";
  17.240 +  "[| is_vectorspace V; x:V |] ==> (- a) (*) - x = a (*) x";
  17.241    by (simp add: negate_eq1);
  17.242  
  17.243  lemma vs_add_minus_left_eq_diff: 
  17.244 @@ -271,11 +271,11 @@
  17.245  qed;
  17.246  
  17.247  lemma vs_add_minus [simp]: 
  17.248 -  "[| is_vectorspace V; x:V |] ==> x + - x = <0>";
  17.249 +  "[| is_vectorspace V; x:V |] ==> x + - x = 00";
  17.250    by (simp! add: diff_eq2);
  17.251  
  17.252  lemma vs_add_minus_left [simp]: 
  17.253 -  "[| is_vectorspace V; x:V |] ==> - x + x = <0>";
  17.254 +  "[| is_vectorspace V; x:V |] ==> - x + x = 00";
  17.255    by (simp! add: diff_eq2);
  17.256  
  17.257  lemma vs_minus_minus [simp]: 
  17.258 @@ -283,11 +283,11 @@
  17.259    by (simp add: negate_eq1);
  17.260  
  17.261  lemma vs_minus_zero [simp]: 
  17.262 -  "is_vectorspace (V::'a::{minus, plus} set) ==> - (<0>::'a) = <0>"; 
  17.263 +  "is_vectorspace (V::'a::{minus, plus} set) ==> - (00::'a) = 00"; 
  17.264    by (simp add: negate_eq1);
  17.265  
  17.266  lemma vs_minus_zero_iff [simp]:
  17.267 -  "[| is_vectorspace V; x:V |] ==> (- x = <0>) = (x = <0>)" 
  17.268 +  "[| is_vectorspace V; x:V |] ==> (- x = 00) = (x = 00)" 
  17.269    (concl is "?L = ?R");
  17.270  proof -;
  17.271    assume "is_vectorspace V" "x:V";
  17.272 @@ -295,7 +295,7 @@
  17.273    proof;
  17.274      have "x = - (- x)"; by (rule vs_minus_minus [RS sym]);
  17.275      also; assume ?L;
  17.276 -    also; have "- ... = <0>"; by (rule vs_minus_zero);
  17.277 +    also; have "- ... = 00"; by (rule vs_minus_zero);
  17.278      finally; show ?R; .;
  17.279    qed (simp!);
  17.280  qed;
  17.281 @@ -314,11 +314,11 @@
  17.282    by (simp add: negate_eq1 vs_add_mult_distrib1);
  17.283  
  17.284  lemma vs_diff_zero [simp]: 
  17.285 -  "[| is_vectorspace V; x:V |] ==> x - <0> = x";
  17.286 +  "[| is_vectorspace V; x:V |] ==> x - 00 = x";
  17.287    by (simp add: diff_eq1);  
  17.288  
  17.289  lemma vs_diff_zero_right [simp]: 
  17.290 -  "[| is_vectorspace V; x:V |] ==> <0> - x = - x";
  17.291 +  "[| is_vectorspace V; x:V |] ==> 00 - x = - x";
  17.292    by (simp add:diff_eq1);
  17.293  
  17.294  lemma vs_add_left_cancel:
  17.295 @@ -327,7 +327,7 @@
  17.296    (concl is "?L = ?R");
  17.297  proof;
  17.298    assume "is_vectorspace V" "x:V" "y:V" "z:V";
  17.299 -  have "y = <0> + y"; by (simp!);
  17.300 +  have "y = 00 + y"; by (simp!);
  17.301    also; have "... = - x + x + y"; by (simp!);
  17.302    also; have "... = - x + (x + y)"; 
  17.303      by (simp! only: vs_add_assoc vs_neg_closed);
  17.304 @@ -350,66 +350,66 @@
  17.305  
  17.306  lemma vs_mult_left_commute: 
  17.307    "[| is_vectorspace V; x:V; y:V; z:V |] 
  17.308 -  ==> x <*> y <*> z = y <*> x <*> z";  
  17.309 +  ==> x (*) y (*) z = y (*) x (*) z";  
  17.310    by (simp add: real_mult_commute);
  17.311  
  17.312  lemma vs_mult_zero_uniq :
  17.313 -  "[| is_vectorspace V; x:V; a <*> x = <0>; x ~= <0> |] ==> a = 0r";
  17.314 +  "[| is_vectorspace V; x:V; a (*) x = 00; x ~= 00 |] ==> a = 0r";
  17.315  proof (rule classical);
  17.316 -  assume "is_vectorspace V" "x:V" "a <*> x = <0>" "x ~= <0>";
  17.317 +  assume "is_vectorspace V" "x:V" "a (*) x = 00" "x ~= 00";
  17.318    assume "a ~= 0r";
  17.319 -  have "x = (rinv a * a) <*> x"; by (simp!);
  17.320 -  also; have "... = rinv a <*> (a <*> x)"; by (rule vs_mult_assoc);
  17.321 -  also; have "... = rinv a <*> <0>"; by (simp!);
  17.322 -  also; have "... = <0>"; by (simp!);
  17.323 -  finally; have "x = <0>"; .;
  17.324 +  have "x = (rinv a * a) (*) x"; by (simp!);
  17.325 +  also; have "... = rinv a (*) (a (*) x)"; by (rule vs_mult_assoc);
  17.326 +  also; have "... = rinv a (*) 00"; by (simp!);
  17.327 +  also; have "... = 00"; by (simp!);
  17.328 +  finally; have "x = 00"; .;
  17.329    thus "a = 0r"; by contradiction; 
  17.330  qed;
  17.331  
  17.332  lemma vs_mult_left_cancel: 
  17.333    "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==> 
  17.334 -  (a <*> x = a <*> y) = (x = y)"
  17.335 +  (a (*) x = a (*) y) = (x = y)"
  17.336    (concl is "?L = ?R");
  17.337  proof;
  17.338    assume "is_vectorspace V" "x:V" "y:V" "a ~= 0r";
  17.339 -  have "x = 1r <*> x"; by (simp!);
  17.340 -  also; have "... = (rinv a * a) <*> x"; by (simp!);
  17.341 -  also; have "... = rinv a <*> (a <*> x)"; 
  17.342 +  have "x = 1r (*) x"; by (simp!);
  17.343 +  also; have "... = (rinv a * a) (*) x"; by (simp!);
  17.344 +  also; have "... = rinv a (*) (a (*) x)"; 
  17.345      by (simp! only: vs_mult_assoc);
  17.346    also; assume ?L;
  17.347 -  also; have "rinv a <*> ... = y"; by (simp!);
  17.348 +  also; have "rinv a (*) ... = y"; by (simp!);
  17.349    finally; show ?R; .;
  17.350  qed simp;
  17.351  
  17.352  lemma vs_mult_right_cancel: (*** forward ***)
  17.353 -  "[| is_vectorspace V; x:V; x ~= <0> |] 
  17.354 -  ==> (a <*> x = b <*> x) = (a = b)" (concl is "?L = ?R");
  17.355 +  "[| is_vectorspace V; x:V; x ~= 00 |] 
  17.356 +  ==> (a (*) x = b (*) x) = (a = b)" (concl is "?L = ?R");
  17.357  proof;
  17.358 -  assume "is_vectorspace V" "x:V" "x ~= <0>";
  17.359 -  have "(a - b) <*> x = a <*> x - b <*> x"; 
  17.360 +  assume "is_vectorspace V" "x:V" "x ~= 00";
  17.361 +  have "(a - b) (*) x = a (*) x - b (*) x"; 
  17.362      by (simp! add: vs_diff_mult_distrib2);
  17.363 -  also; assume ?L; hence "a <*> x - b <*> x = <0>"; by (simp!);
  17.364 -  finally; have "(a - b) <*> x = <0>"; .; 
  17.365 +  also; assume ?L; hence "a (*) x - b (*) x = 00"; by (simp!);
  17.366 +  finally; have "(a - b) (*) x = 00"; .; 
  17.367    hence "a - b = 0r"; by (simp! add: vs_mult_zero_uniq);
  17.368    thus "a = b"; by (rule real_add_minus_eq);
  17.369  qed simp; (*** 
  17.370  
  17.371  backward :
  17.372  lemma vs_mult_right_cancel: 
  17.373 -  "[| is_vectorspace V; x:V; x ~= <0> |] ==>  
  17.374 -  (a <*> x = b <*> x) = (a = b)"
  17.375 +  "[| is_vectorspace V; x:V; x ~= 00 |] ==>  
  17.376 +  (a ( * ) x = b ( * ) x) = (a = b)"
  17.377    (concl is "?L = ?R");
  17.378  proof;
  17.379 -  assume "is_vectorspace V" "x:V" "x ~= <0>";
  17.380 +  assume "is_vectorspace V" "x:V" "x ~= 00";
  17.381    assume l: ?L; 
  17.382    show "a = b"; 
  17.383    proof (rule real_add_minus_eq);
  17.384      show "a - b = 0r"; 
  17.385      proof (rule vs_mult_zero_uniq);
  17.386 -      have "(a - b) <*> x = a <*> x - b <*> x";
  17.387 +      have "(a - b) ( * ) x = a ( * ) x - b ( * ) x";
  17.388          by (simp! add: vs_diff_mult_distrib2);
  17.389 -      also; from l; have "a <*> x - b <*> x = <0>"; by (simp!);
  17.390 -      finally; show "(a - b) <*> x  = <0>"; .; 
  17.391 +      also; from l; have "a ( * ) x - b ( * ) x = 00"; by (simp!);
  17.392 +      finally; show "(a - b) ( * ) x  = 00"; .; 
  17.393      qed;
  17.394    qed;
  17.395  next;
  17.396 @@ -431,7 +431,7 @@
  17.397      also; have "... = z + - y + y"; by (simp! add: diff_eq1);
  17.398      also; have "... = z + (- y + y)"; 
  17.399        by (rule vs_add_assoc) (simp!)+;
  17.400 -    also; from vs; have "... = z + <0>"; 
  17.401 +    also; from vs; have "... = z + 00"; 
  17.402        by (simp only: vs_add_minus_left);
  17.403      also; from vs; have "... = z"; by (simp only: vs_add_zero_right);
  17.404      finally; show ?R; .;
  17.405 @@ -448,22 +448,22 @@
  17.406  qed;
  17.407  
  17.408  lemma vs_add_minus_eq_minus: 
  17.409 -  "[| is_vectorspace V; x:V; y:V; x + y = <0> |] ==> x = - y"; 
  17.410 +  "[| is_vectorspace V; x:V; y:V; x + y = 00 |] ==> x = - y"; 
  17.411  proof -;
  17.412    assume "is_vectorspace V" "x:V" "y:V"; 
  17.413    have "x = (- y + y) + x"; by (simp!);
  17.414    also; have "... = - y + (x + y)"; by (simp!);
  17.415 -  also; assume "x + y = <0>";
  17.416 -  also; have "- y + <0> = - y"; by (simp!);
  17.417 +  also; assume "x + y = 00";
  17.418 +  also; have "- y + 00 = - y"; by (simp!);
  17.419    finally; show "x = - y"; .;
  17.420  qed;
  17.421  
  17.422  lemma vs_add_minus_eq: 
  17.423 -  "[| is_vectorspace V; x:V; y:V; x - y = <0> |] ==> x = y"; 
  17.424 +  "[| is_vectorspace V; x:V; y:V; x - y = 00 |] ==> x = y"; 
  17.425  proof -;
  17.426 -  assume "is_vectorspace V" "x:V" "y:V" "x - y = <0>";
  17.427 -  assume "x - y = <0>";
  17.428 -  hence e: "x + - y = <0>"; by (simp! add: diff_eq1);
  17.429 +  assume "is_vectorspace V" "x:V" "y:V" "x - y = 00";
  17.430 +  assume "x - y = 00";
  17.431 +  hence e: "x + - y = 00"; by (simp! add: diff_eq1);
  17.432    with _ _ _; have "x = - (- y)"; 
  17.433      by (rule vs_add_minus_eq_minus) (simp!)+;
  17.434    thus "x = y"; by (simp!);
  17.435 @@ -514,12 +514,12 @@
  17.436    show "?L = ?R";
  17.437    proof;
  17.438      assume l: ?L;
  17.439 -    have "x + z = <0>"; 
  17.440 +    have "x + z = 00"; 
  17.441      proof (rule vs_add_left_cancel [RS iffD1]);
  17.442        have "y + (x + z) = x + (y + z)"; by (simp!);
  17.443        also; note l;
  17.444 -      also; have "y = y + <0>"; by (simp!);
  17.445 -      finally; show "y + (x + z) = y + <0>"; .;
  17.446 +      also; have "y = y + 00"; by (simp!);
  17.447 +      finally; show "y + (x + z) = y + 00"; .;
  17.448      qed (simp!)+;
  17.449      thus "x = - z"; by (simp! add: vs_add_minus_eq_minus);
  17.450    next;
  17.451 @@ -532,4 +532,4 @@
  17.452    qed;
  17.453  qed;
  17.454  
  17.455 -end;
  17.456 \ No newline at end of file
  17.457 +end;
    18.1 --- a/src/HOL/Relation.ML	Thu Apr 13 15:01:45 2000 +0200
    18.2 +++ b/src/HOL/Relation.ML	Thu Apr 13 15:01:50 2000 +0200
    18.3 @@ -63,7 +63,7 @@
    18.4  by (Blast_tac 1);
    18.5  qed "diag_iff";
    18.6  
    18.7 -Goal "diag(A) <= A Times A";
    18.8 +Goal "diag(A) <= A <*> A";
    18.9  by (Blast_tac 1);
   18.10  qed "diag_subset_Times";
   18.11  
   18.12 @@ -115,14 +115,14 @@
   18.13  by (Blast_tac 1);
   18.14  qed "comp_mono";
   18.15  
   18.16 -Goal "[| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
   18.17 +Goal "[| s <= A <*> B;  r <= B <*> C |] ==> (r O s) <= A <*> C";
   18.18  by (Blast_tac 1);
   18.19  qed "comp_subset_Sigma";
   18.20  
   18.21  (** Natural deduction for refl(r) **)
   18.22  
   18.23  val prems = Goalw [refl_def]
   18.24 -    "[| r <= A Times A;  !! x. x:A ==> (x,x):r |] ==> refl A r";
   18.25 +    "[| r <= A <*> A;  !! x. x:A ==> (x,x):r |] ==> refl A r";
   18.26  by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
   18.27  qed "reflI";
   18.28  
   18.29 @@ -371,7 +371,7 @@
   18.30  by (Blast_tac 1);
   18.31  qed "Image_Un";
   18.32  
   18.33 -Goal "r <= A Times B ==> r^^C <= B";
   18.34 +Goal "r <= A <*> B ==> r^^C <= B";
   18.35  by (rtac subsetI 1);
   18.36  by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
   18.37  qed "Image_subset";
    19.1 --- a/src/HOL/Relation.thy	Thu Apr 13 15:01:45 2000 +0200
    19.2 +++ b/src/HOL/Relation.thy	Thu Apr 13 15:01:50 2000 +0200
    19.3 @@ -29,7 +29,7 @@
    19.4      "Range(r) == Domain(r^-1)"
    19.5  
    19.6    refl   :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
    19.7 -    "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)"
    19.8 +    "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)"
    19.9  
   19.10    sym    :: "('a*'a) set=>bool"             (*symmetry predicate*)
   19.11      "sym(r) == ALL x y. (x,y): r --> (y,x): r"
    20.1 --- a/src/HOL/Sexp.ML	Thu Apr 13 15:01:45 2000 +0200
    20.2 +++ b/src/HOL/Sexp.ML	Thu Apr 13 15:01:50 2000 +0200
    20.3 @@ -49,7 +49,7 @@
    20.4  
    20.5  (** Introduction rules for 'pred_sexp' **)
    20.6  
    20.7 -Goalw [pred_sexp_def] "pred_sexp <= sexp Times sexp";
    20.8 +Goalw [pred_sexp_def] "pred_sexp <= sexp <*> sexp";
    20.9  by (Blast_tac 1);
   20.10  qed "pred_sexp_subset_Sigma";
   20.11  
    21.1 --- a/src/HOL/Subst/Unify.thy	Thu Apr 13 15:01:45 2000 +0200
    21.2 +++ b/src/HOL/Subst/Unify.thy	Thu Apr 13 15:01:50 2000 +0200
    21.3 @@ -19,7 +19,7 @@
    21.4      --either the set of variables decreases
    21.5      --or the first argument does (in fact, both do)
    21.6    *)
    21.7 -  unifyRel_def  "unifyRel == inv_image  (finite_psubset ** measure uterm_size)
    21.8 +  unifyRel_def  "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size)
    21.9                                 (%(M,N). (vars_of M Un vars_of N, M))"
   21.10  
   21.11  recdef unify "unifyRel"
    22.1 --- a/src/HOL/Trancl.ML	Thu Apr 13 15:01:45 2000 +0200
    22.2 +++ b/src/HOL/Trancl.ML	Thu Apr 13 15:01:50 2000 +0200
    22.3 @@ -342,12 +342,12 @@
    22.4  by (auto_tac (claset() addIs [r_into_trancl], simpset()));
    22.5  qed "irrefl_tranclI";
    22.6  
    22.7 -Goal "[| (a,b) : r^*;  r <= A Times A |] ==> a=b | a:A";
    22.8 +Goal "[| (a,b) : r^*;  r <= A <*> A |] ==> a=b | a:A";
    22.9  by (etac rtrancl_induct 1);
   22.10  by Auto_tac;
   22.11  val lemma = result();
   22.12  
   22.13 -Goalw [trancl_def] "r <= A Times A ==> r^+ <= A Times A";
   22.14 +Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
   22.15  by (blast_tac (claset() addSDs [lemma]) 1);
   22.16  qed "trancl_subset_Sigma";
   22.17  
    23.1 --- a/src/HOL/UNITY/Extend.thy	Thu Apr 13 15:01:45 2000 +0200
    23.2 +++ b/src/HOL/UNITY/Extend.thy	Thu Apr 13 15:01:50 2000 +0200
    23.3 @@ -17,7 +17,7 @@
    23.4       (*Using the locale constant "f", this is  f (h (x,y))) = x*)
    23.5    
    23.6    extend_set :: "['a*'b => 'c, 'a set] => 'c set"
    23.7 -    "extend_set h A == h `` (A Times UNIV)"
    23.8 +    "extend_set h A == h `` (A <*> UNIV)"
    23.9  
   23.10    project_set :: "['a*'b => 'c, 'c set] => 'a set"
   23.11      "project_set h C == {x. EX y. h(x,y) : C}"
    24.1 --- a/src/HOL/UNITY/LessThan.thy	Thu Apr 13 15:01:45 2000 +0200
    24.2 +++ b/src/HOL/UNITY/LessThan.thy	Thu Apr 13 15:01:50 2000 +0200
    24.3 @@ -14,7 +14,7 @@
    24.4  
    24.5    (*MOVE TO RELATION.THY??*)
    24.6    Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
    24.7 -    "Restrict A r == r Int (A Times UNIV)"
    24.8 +    "Restrict A r == r Int (A <*> UNIV)"
    24.9  
   24.10    lessThan   :: "nat => nat set"
   24.11       "lessThan n == {i. i<n}"
    25.1 --- a/src/HOL/UNITY/Lift_prog.ML	Thu Apr 13 15:01:45 2000 +0200
    25.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Thu Apr 13 15:01:50 2000 +0200
    25.3 @@ -254,20 +254,20 @@
    25.4  by (Force_tac 1);
    25.5  qed "delete_map_neq_apply";
    25.6  
    25.7 -(*A set of the form (A Times UNIV) ignores the second (dummy) state component*)
    25.8 +(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
    25.9  
   25.10 -Goal "(f o fst) -`` A = (f-``A) Times UNIV";
   25.11 +Goal "(f o fst) -`` A = (f-``A) <*> UNIV";
   25.12  by Auto_tac;
   25.13  qed "vimage_o_fst_eq";
   25.14  
   25.15 -Goal "(sub i -``A) Times UNIV = lift_set i (A Times UNIV)";
   25.16 +Goal "(sub i -``A) <*> UNIV = lift_set i (A <*> UNIV)";
   25.17  by Auto_tac;
   25.18  qed "vimage_sub_eq_lift_set";
   25.19  
   25.20  Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set];
   25.21  
   25.22  Goal "[| F : preserves snd;  i~=j |] \
   25.23 -\     ==> lift j F : stable (lift_set i (A Times UNIV))";
   25.24 +\     ==> lift j F : stable (lift_set i (A <*> UNIV))";
   25.25  by (auto_tac (claset(),
   25.26  	      simpset() addsimps [lift_def, lift_set_def, 
   25.27  				  stable_def, constrains_def, 
   25.28 @@ -280,9 +280,9 @@
   25.29  
   25.30  (*If i~=j then lift j F  does nothing to lift_set i, and the 
   25.31    premise ensures A<=B.*)
   25.32 -Goal "[| F i : (A Times UNIV) co (B Times UNIV);  \
   25.33 +Goal "[| F i : (A <*> UNIV) co (B <*> UNIV);  \
   25.34  \        F j : preserves snd |]  \
   25.35 -\  ==> lift j (F j) : (lift_set i (A Times UNIV)) co (lift_set i (B Times UNIV))";
   25.36 +\  ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))";
   25.37  by (case_tac "i=j" 1);
   25.38  by (asm_full_simp_tac (simpset() addsimps [lift_def, lift_set_def, 
   25.39  					   rename_constrains]) 1);
   25.40 @@ -323,8 +323,8 @@
   25.41  qed "lift_map_eq_diff";
   25.42  
   25.43  Goal "F : preserves snd \
   25.44 -\     ==> (lift i F : transient (lift_set j (A Times UNIV))) = \
   25.45 -\         (i=j & F : transient (A Times UNIV) | A={})";
   25.46 +\     ==> (lift i F : transient (lift_set j (A <*> UNIV))) = \
   25.47 +\         (i=j & F : transient (A <*> UNIV) | A={})";
   25.48  by (case_tac "i=j" 1);
   25.49  by (auto_tac (claset(), simpset() addsimps [lift_transient]));
   25.50  by (auto_tac (claset(),
   25.51 @@ -349,8 +349,8 @@
   25.52  qed "lift_transient_eq_disj";
   25.53  
   25.54  (*USELESS??*)
   25.55 -Goal "lift_map i `` (A Times UNIV) = \
   25.56 -\     (UN s:A. UN f. {insert_map i s f}) Times UNIV";
   25.57 +Goal "lift_map i `` (A <*> UNIV) = \
   25.58 +\     (UN s:A. UN f. {insert_map i s f}) <*> UNIV";
   25.59  by (auto_tac (claset() addSIs [bexI, image_eqI],
   25.60                simpset() addsimps [lift_map_def]));
   25.61  by (rtac (split RS sym) 1);
    26.1 --- a/src/HOL/UNITY/PPROD.ML	Thu Apr 13 15:01:45 2000 +0200
    26.2 +++ b/src/HOL/UNITY/PPROD.ML	Thu Apr 13 15:01:50 2000 +0200
    26.3 @@ -49,9 +49,9 @@
    26.4  (** Safety & Progress **)
    26.5  
    26.6  Goal "[| i : I;  ALL j. F j : preserves snd |] ==>  \
    26.7 -\     (PLam I F : (lift_set i (A Times UNIV)) co \
    26.8 -\                 (lift_set i (B Times UNIV)))  =  \
    26.9 -\     (F i : (A Times UNIV) co (B Times UNIV))";
   26.10 +\     (PLam I F : (lift_set i (A <*> UNIV)) co \
   26.11 +\                 (lift_set i (B <*> UNIV)))  =  \
   26.12 +\     (F i : (A <*> UNIV) co (B <*> UNIV))";
   26.13  by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains,
   26.14  				      Join_constrains]) 1);
   26.15  by (stac (insert_Diff RS sym) 1 THEN assume_tac 1);
   26.16 @@ -60,8 +60,8 @@
   26.17  qed "PLam_constrains";
   26.18  
   26.19  Goal "[| i : I;  ALL j. F j : preserves snd |]  \
   26.20 -\     ==> (PLam I F : stable (lift_set i (A Times UNIV))) = \
   26.21 -\         (F i : stable (A Times UNIV))";
   26.22 +\     ==> (PLam I F : stable (lift_set i (A <*> UNIV))) = \
   26.23 +\         (F i : stable (A <*> UNIV))";
   26.24  by (asm_simp_tac (simpset() addsimps [stable_def, PLam_constrains]) 1);
   26.25  qed "PLam_stable";
   26.26  
   26.27 @@ -73,9 +73,9 @@
   26.28  Addsimps [PLam_constrains, PLam_stable, PLam_transient];
   26.29  
   26.30  (*This holds because the F j cannot change (lift_set i)*)
   26.31 -Goal "[| i : I;  F i : (A Times UNIV) ensures (B Times UNIV);  \
   26.32 +Goal "[| i : I;  F i : (A <*> UNIV) ensures (B <*> UNIV);  \
   26.33  \        ALL j. F j : preserves snd |] ==>  \
   26.34 -\     PLam I F : lift_set i (A Times UNIV) ensures lift_set i (B Times UNIV)";
   26.35 +\     PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)";
   26.36  by (auto_tac (claset(), 
   26.37  	      simpset() addsimps [ensures_def, lift_transient_eq_disj,
   26.38  				  lift_set_Un_distrib RS sym,
   26.39 @@ -85,11 +85,11 @@
   26.40  qed "PLam_ensures";
   26.41  
   26.42  Goal "[| i : I;  \
   26.43 -\        F i : ((A Times UNIV) - (B Times UNIV)) co \
   26.44 -\              ((A Times UNIV) Un (B Times UNIV));  \
   26.45 -\        F i : transient ((A Times UNIV) - (B Times UNIV));  \
   26.46 +\        F i : ((A <*> UNIV) - (B <*> UNIV)) co \
   26.47 +\              ((A <*> UNIV) Un (B <*> UNIV));  \
   26.48 +\        F i : transient ((A <*> UNIV) - (B <*> UNIV));  \
   26.49  \        ALL j. F j : preserves snd |] ==>  \
   26.50 -\     PLam I F : lift_set i (A Times UNIV) leadsTo lift_set i (B Times UNIV)";
   26.51 +\     PLam I F : lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)";
   26.52  by (rtac (PLam_ensures RS leadsTo_Basis) 1);
   26.53  by (rtac ensuresI 2);
   26.54  by (ALLGOALS assume_tac);
   26.55 @@ -98,9 +98,9 @@
   26.56  
   26.57  (** invariant **)
   26.58  
   26.59 -Goal "[| F i : invariant (A Times UNIV);  i : I;  \
   26.60 +Goal "[| F i : invariant (A <*> UNIV);  i : I;  \
   26.61  \        ALL j. F j : preserves snd |] \
   26.62 -\     ==> PLam I F : invariant (lift_set i (A Times UNIV))";
   26.63 +\     ==> PLam I F : invariant (lift_set i (A <*> UNIV))";
   26.64  by (auto_tac (claset(),
   26.65  	      simpset() addsimps [invariant_def]));
   26.66  qed "invariant_imp_PLam_invariant";
    27.1 --- a/src/HOL/UNITY/TimerArray.ML	Thu Apr 13 15:01:45 2000 +0200
    27.2 +++ b/src/HOL/UNITY/TimerArray.ML	Thu Apr 13 15:01:50 2000 +0200
    27.3 @@ -29,7 +29,7 @@
    27.4  
    27.5  Goal "finite I \
    27.6  \     ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}";
    27.7 -by (eres_inst_tac [("A'1", "%i. lift_set i ({0} Times UNIV)")]
    27.8 +by (eres_inst_tac [("A'1", "%i. lift_set i ({0} <*> UNIV)")]
    27.9      (finite_stable_completion RS leadsTo_weaken) 1);
   27.10  by Auto_tac;
   27.11  (*Safety property, already reduced to the single Timer case*)
   27.12 @@ -37,7 +37,7 @@
   27.13  (*Progress property for the array of Timers*)
   27.14  by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
   27.15  by (case_tac "m" 1);
   27.16 -(*Annoying need to massage the conditions to have the form (... Times UNIV)*)
   27.17 +(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
   27.18  by (auto_tac (claset() addIs [subset_imp_leadsTo], 
   27.19  	      simpset() addsimps [insert_absorb, lessThan_Suc RS sym,
   27.20  				  lift_set_Un_distrib RS sym,
    28.1 --- a/src/HOL/UNITY/Token.thy	Thu Apr 13 15:01:45 2000 +0200
    28.2 +++ b/src/HOL/UNITY/Token.thy	Thu Apr 13 15:01:50 2000 +0200
    28.3 @@ -58,7 +58,7 @@
    28.4    defines
    28.5      nodeOrder_def
    28.6        "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
    28.7 -		      (lessThan N Times lessThan N)"
    28.8 +		      (lessThan N <*> lessThan N)"
    28.9  
   28.10      next_def
   28.11        "next i == (Suc i) mod N"
    29.1 --- a/src/HOL/UNITY/UNITY.ML	Thu Apr 13 15:01:45 2000 +0200
    29.2 +++ b/src/HOL/UNITY/UNITY.ML	Thu Apr 13 15:01:50 2000 +0200
    29.3 @@ -14,24 +14,6 @@
    29.4  Delsimps [image_Collect];
    29.5  
    29.6  
    29.7 -(*** General lemmas ***)
    29.8 -
    29.9 -Goal "UNIV Times UNIV = UNIV";
   29.10 -by Auto_tac;
   29.11 -qed "UNIV_Times_UNIV"; 
   29.12 -Addsimps [UNIV_Times_UNIV];
   29.13 -
   29.14 -Goal "- (UNIV Times A) = UNIV Times (-A)";
   29.15 -by Auto_tac;
   29.16 -qed "Compl_Times_UNIV1"; 
   29.17 -
   29.18 -Goal "- (A Times UNIV) = (-A) Times UNIV";
   29.19 -by Auto_tac;
   29.20 -qed "Compl_Times_UNIV2"; 
   29.21 -
   29.22 -Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; 
   29.23 -
   29.24 -
   29.25  (*** The abstract type of programs ***)
   29.26  
   29.27  val rep_ss = simpset() addsimps 
    30.1 --- a/src/HOL/Univ.ML	Thu Apr 13 15:01:45 2000 +0200
    30.2 +++ b/src/HOL/Univ.ML	Thu Apr 13 15:01:50 2000 +0200
    30.3 @@ -582,7 +582,7 @@
    30.4  
    30.5  (*** Bounding theorems ***)
    30.6  
    30.7 -Goal "(dprod (A Times B) (C Times D)) <= (uprod A C) Times (uprod B D)";
    30.8 +Goal "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)";
    30.9  by (Blast_tac 1);
   30.10  qed "dprod_Sigma";
   30.11  
   30.12 @@ -595,7 +595,7 @@
   30.13  by (Blast_tac 1);
   30.14  qed "dprod_subset_Sigma2";
   30.15  
   30.16 -Goal "(dsum (A Times B) (C Times D)) <= (usum A C) Times (usum B D)";
   30.17 +Goal "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)";
   30.18  by (Blast_tac 1);
   30.19  qed "dsum_Sigma";
   30.20  
    31.1 --- a/src/HOL/WF.ML	Thu Apr 13 15:01:45 2000 +0200
    31.2 +++ b/src/HOL/WF.ML	Thu Apr 13 15:01:50 2000 +0200
    31.3 @@ -20,7 +20,7 @@
    31.4  
    31.5  (*Restriction to domain A.  If r is well-founded over A then wf(r)*)
    31.6  val [prem1,prem2] = Goalw [wf_def]
    31.7 - "[| r <= A Times A;  \
    31.8 + "[| r <= A <*> A;  \
    31.9  \    !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x);  x:A |] ==> P(x) |]  \
   31.10  \ ==>  wf(r)";
   31.11  by (blast_tac (claset() addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
    32.1 --- a/src/HOL/WF_Rel.ML	Thu Apr 13 15:01:45 2000 +0200
    32.2 +++ b/src/HOL/WF_Rel.ML	Thu Apr 13 15:01:50 2000 +0200
    32.3 @@ -73,7 +73,7 @@
    32.4   *---------------------------------------------------------------------------*)
    32.5  
    32.6  val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
    32.7 - "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
    32.8 + "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)";
    32.9  by (EVERY1 [rtac allI,rtac impI]);
   32.10  by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
   32.11  by (rtac (wfa RS spec RS mp) 1);
   32.12 @@ -87,7 +87,7 @@
   32.13   * Transitivity of WF combinators.
   32.14   *---------------------------------------------------------------------------*)
   32.15  Goalw [trans_def, lex_prod_def]
   32.16 -    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)";
   32.17 +    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)";
   32.18  by (Simp_tac 1);
   32.19  by (Blast_tac 1);
   32.20  qed "trans_lex_prod";
    33.1 --- a/src/HOL/WF_Rel.thy	Thu Apr 13 15:01:45 2000 +0200
    33.2 +++ b/src/HOL/WF_Rel.thy	Thu Apr 13 15:01:50 2000 +0200
    33.3 @@ -19,7 +19,8 @@
    33.4    less_than :: "(nat*nat)set"
    33.5    inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
    33.6    measure   :: "('a => nat) => ('a * 'a)set"
    33.7 -  "**"      :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
    33.8 +  lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
    33.9 +               (infixr "<*lex*>" 80)
   33.10    finite_psubset  :: "('a set * 'a set) set"
   33.11  
   33.12  
   33.13 @@ -30,9 +31,8 @@
   33.14  
   33.15    measure_def   "measure == inv_image less_than"
   33.16  
   33.17 -  lex_prod_def  "ra**rb == {p. ? a a' b b'. 
   33.18 -                                p = ((a,b),(a',b')) & 
   33.19 -                               ((a,a') : ra | a=a' & (b,b') : rb)}"
   33.20 +  lex_prod_def  "ra <*lex*> rb == {((a,b),(a',b')) | a a' b b'.
   33.21 +                                   ((a,a') : ra | a=a' & (b,b') : rb)}"
   33.22  
   33.23    (* finite proper subset*)
   33.24    finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}"
    34.1 --- a/src/HOL/ex/Primrec.thy	Thu Apr 13 15:01:45 2000 +0200
    34.2 +++ b/src/HOL/ex/Primrec.thy	Thu Apr 13 15:01:50 2000 +0200
    34.3 @@ -19,7 +19,7 @@
    34.4  Primrec = Main +
    34.5  
    34.6  consts ack  :: "nat * nat => nat"
    34.7 -recdef ack "less_than ** less_than"
    34.8 +recdef ack "less_than <*lex*> less_than"
    34.9      "ack (0,n) =  Suc n"
   34.10      "ack (Suc m,0) = (ack (m, 1))"
   34.11      "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"
    35.1 --- a/src/HOL/ex/Tarski.ML	Thu Apr 13 15:01:45 2000 +0200
    35.2 +++ b/src/HOL/ex/Tarski.ML	Thu Apr 13 15:01:50 2000 +0200
    35.3 @@ -540,7 +540,7 @@
    35.4  qed "T_thm_1_glb";
    35.5  
    35.6  (* interval *)
    35.7 -Goal "refl A r ==> r <= A Times A";
    35.8 +Goal "refl A r ==> r <= A <*> A";
    35.9  by (afs [refl_def] 1);
   35.10  qed "reflE1";
   35.11