# HG changeset patch
# User wenzelm
# Date 1451250437 -3600
# Node ID 7fba644ed827e6bcde19bcd7f3ce4e72c8449ee4
# Parent  f02b26f7d39da49eba0eb3abc6054c3469e9f20e
discontinued ASCII replacement syntax <*>;

diff -r f02b26f7d39d -r 7fba644ed827 NEWS
--- a/NEWS	Sun Dec 27 21:46:36 2015 +0100
+++ b/NEWS	Sun Dec 27 22:07:17 2015 +0100
@@ -476,6 +476,8 @@
 
   notation iff  (infixr "<->" 25)
 
+  notation Times  (infixr "<*>" 80)
+
   type_notation Map.map  (infixr "~=>" 0)
   notation Map.map_comp  (infixl "o'_m" 55)
 
diff -r f02b26f7d39d -r 7fba644ed827 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/Doc/Main/Main_Doc.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -228,7 +228,7 @@
 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
 @{term"Pair a b"} & @{term[source]"Pair a b"}\\
 @{term"case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
-@{term"A <*> B"} &  @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$)
+@{term"A \<times> B"} &  @{text"Sigma A (\<lambda>\<^raw:\_>. B)"}
 \end{tabular}
 
 Pairs may be nested. Nesting to the right is printed as a tuple,
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/BNF_Cardinal_Arithmetic.thy
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -281,7 +281,7 @@
 subsection \<open>Product\<close>
 
 definition cprod (infixr "*c" 80) where
-  "r1 *c r2 = |Field r1 <*> Field r2|"
+  "r1 *c r2 = |Field r1 \<times> Field r2|"
 
 lemma card_order_cprod:
   assumes "card_order r1" "card_order r2"
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/BNF_Cardinal_Order_Relation.thy
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -788,7 +788,7 @@
 qed
 
 lemma card_of_Times_Plus_distrib:
-  "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|")
+  "|A \<times> (B <+> C)| =o |A \<times> B <+> A \<times> C|" (is "|?RHS| =o |?LHS|")
 proof -
   let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
   have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
@@ -1038,7 +1038,7 @@
 
 lemma card_of_Times_ordLeq_infinite_Field:
 "\<lbrakk>\<not>finite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
- \<Longrightarrow> |A <*> B| \<le>o r"
+ \<Longrightarrow> |A \<times> B| \<le>o r"
 by(simp add: card_of_Sigma_ordLeq_infinite_Field)
 
 lemma card_of_Times_infinite_simps:
@@ -1619,7 +1619,7 @@
 subsection \<open>Others\<close>
 
 lemma card_of_Func_Times:
-"|Func (A <*> B) C| =o |Func A (Func B C)|"
+"|Func (A \<times> B) C| =o |Func A (Func B C)|"
 unfolding card_of_ordIso[symmetric]
 using bij_betw_curr by blast
 
@@ -1661,7 +1661,7 @@
 qed
 
 lemma Func_Times_Range:
-  "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|")
+  "|Func A (B \<times> C)| =o |Func A B \<times> Func A C|" (is "|?LHS| =o |?RHS|")
 proof -
   let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined,
                   \<lambda>x. if x \<in> A then snd (fg x) else undefined)"
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/BNF_Greatest_Fixpoint.thy
--- a/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -73,7 +73,7 @@
 lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
   unfolding Gr_def by simp
 
-lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
+lemma Gr_incl: "Gr A f \<subseteq> A \<times> B \<longleftrightarrow> f ` A \<subseteq> B"
   unfolding Gr_def by auto
 
 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
@@ -137,7 +137,7 @@
   by (auto simp: proj_preserves)
 
 lemma relImage_relInvImage:
-  assumes "R \<subseteq> f ` A <*> f ` A"
+  assumes "R \<subseteq> f ` A \<times> f ` A"
   shows "relImage (relInvImage A R f) f = R"
   using assms unfolding relImage_def relInvImage_def by fast
 
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/BNF_Wellorder_Constructions.thy
--- a/src/HOL/BNF_Wellorder_Constructions.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -1515,19 +1515,19 @@
 "curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
 
 lemma curr_in:
-assumes f: "f \<in> Func (A <*> B) C"
+assumes f: "f \<in> Func (A \<times> B) C"
 shows "curr A f \<in> Func A (Func B C)"
 using assms unfolding curr_def Func_def by auto
 
 lemma curr_inj:
-assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C"
+assumes "f1 \<in> Func (A \<times> B) C" and "f2 \<in> Func (A \<times> B) C"
 shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
 proof safe
   assume c: "curr A f1 = curr A f2"
   show "f1 = f2"
   proof (rule ext, clarify)
     fix a b show "f1 (a, b) = f2 (a, b)"
-    proof (cases "(a,b) \<in> A <*> B")
+    proof (cases "(a,b) \<in> A \<times> B")
       case False
       thus ?thesis using assms unfolding Func_def by auto
     next
@@ -1540,7 +1540,7 @@
 
 lemma curr_surj:
 assumes "g \<in> Func A (Func B C)"
-shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g"
+shows "\<exists> f \<in> Func (A \<times> B) C. curr A f = g"
 proof
   let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"
   show "curr A ?f = g"
@@ -1557,11 +1557,11 @@
       thus ?thesis using True unfolding Func_def curr_def by auto
     qed
   qed
-  show "?f \<in> Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto
+  show "?f \<in> Func (A \<times> B) C" using assms unfolding Func_def mem_Collect_eq by auto
 qed
 
 lemma bij_betw_curr:
-"bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))"
+"bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))"
 unfolding bij_betw_def inj_on_def image_def
 apply (intro impI conjI ballI)
 apply (erule curr_inj[THEN iffD1], assumption+)
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -51,8 +51,8 @@
 shows "|A \<times> {x}| =o |A|"
 proof -
   def f \<equiv> "\<lambda>(a::'a,b::'b). (a)"
-  have "A \<subseteq> f ` (A <*> {x})" unfolding f_def by (auto simp: image_iff)
-  hence "bij_betw f (A <*> {x}) A"  unfolding bij_betw_def inj_on_def f_def by fastforce
+  have "A \<subseteq> f ` (A \<times> {x})" unfolding f_def by (auto simp: image_iff)
+  hence "bij_betw f (A \<times> {x}) A"  unfolding bij_betw_def inj_on_def f_def by fastforce
   thus ?thesis using card_of_ordIso by blast
 qed
 
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -489,7 +489,7 @@
 
 lemma card_of_Times_ordLeq_infinite:
 "\<lbrakk>\<not>finite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
- \<Longrightarrow> |A <*> B| \<le>o |C|"
+ \<Longrightarrow> |A \<times> B| \<le>o |C|"
 by(simp add: card_of_Sigma_ordLeq_infinite)
 
 corollary Plus_infinite_bij_betw:
@@ -621,7 +621,7 @@
   ordIso_symmetric by blast
   hence "|A| <o |?C|"  "|B| <o |?C|"
   using LESS1 LESS2 ordLess_ordIso_trans by blast+
-  hence  "|A <*> B| <o |?C|" using INF
+  hence  "|A \<times> B| <o |?C|" using INF
   card_of_Times_ordLess_infinite by blast
   thus ?thesis using 1 ordLess_ordIso_trans by blast
 qed
@@ -1502,12 +1502,12 @@
 
 lemma card_of_Pfunc_Pow_Func_option:
 assumes "B \<noteq> {}"
-shows "|Pfunc A B| \<le>o |Pow A <*> Func_option A B|"
+shows "|Pfunc A B| \<le>o |Pow A \<times> Func_option A B|"
 proof-
   have "|Pfunc A B| =o |\<Union>A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
     unfolding Pfunc_Func_option by(rule card_of_refl)
   also have "?K \<le>o |Sigma (Pow A) (\<lambda> A'. Func_option A' B)|" using card_of_UNION_Sigma .
-  also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A <*> Func_option A B|"
+  also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A \<times> Func_option A B|"
     apply(rule card_of_Sigma_mono1) using card_of_Func_option_mono[OF _ assms] by auto
   finally show ?thesis .
 qed
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Groups_Big.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -350,7 +350,7 @@
 qed
 
 lemma cartesian_product:
-   "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A <*> B)"
+   "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A \<times> B)"
 apply (rule sym)
 apply (cases "finite A") 
  apply (cases "finite B") 
@@ -1032,15 +1032,15 @@
 
 (*
 lemma SigmaI_insert: "y \<notin> A ==>
-  (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
+  (SIGMA x:(insert y A). B x) = (({y} \<times> (B y)) \<union> (SIGMA x: A. B x))"
   by auto
 *)
 
-lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
+lemma card_cartesian_product: "card (A \<times> B) = card(A) * card(B)"
   by (cases "finite A \<and> finite B")
     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
 
-lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
+lemma card_cartesian_product_singleton:  "card({x} \<times> A) = card(A)"
 by (simp add: card_cartesian_product)
 
 
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Induct/SList.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -10,8 +10,8 @@
 
 Definition of type 'a list (strict lists) by a least fixed point
 
-We use          list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
-and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
+We use          list(A) == lfp(%Z. {NUMB(0)} <+> A \<times> Z)
+and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) \<times> Z)
 
 so that list can serve as a "functor" for defining other recursive types.
 
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Induct/Sexp.thy
--- a/src/HOL/Induct/Sexp.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Induct/Sexp.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -74,7 +74,7 @@
 
 (** Introduction rules for 'pred_sexp' **)
 
-lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp"
+lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp \<times> sexp"
   by (simp add: pred_sexp_def) blast
 
 (* (a,b) \<in> pred_sexp^+ ==> a \<in> sexp *)
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -3108,7 +3108,7 @@
     setsum (\<lambda>(k,m). a$k * b$m * (c^k * d^m) $ n) {(k,m). k + m \<le> n}"  (is "?l = ?r")
 proof -
   let ?S = "{(k::nat, m::nat). k + m \<le> n}"
-  have s: "?S \<subseteq> {0..n} <*> {0..n}" by (auto simp add: subset_eq)
+  have s: "?S \<subseteq> {0..n} \<times> {0..n}" by (auto simp add: subset_eq)
   have f: "finite {(k::nat, m::nat). k + m \<le> n}"
     apply (rule finite_subset[OF s])
     apply auto
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Library/Old_Datatype.thy
--- a/src/HOL/Library/Old_Datatype.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Library/Old_Datatype.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -495,7 +495,7 @@
 
 (*** Bounding theorems ***)
 
-lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"
+lemma dprod_Sigma: "(dprod (A \<times> B) (C \<times> D)) <= (uprod A C) \<times> (uprod B D)"
 by blast
 
 lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma]
@@ -505,7 +505,7 @@
     "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
 by auto
 
-lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"
+lemma dsum_Sigma: "(dsum (A \<times> B) (C \<times> D)) <= (usum A C) \<times> (usum B D)"
 by blast
 
 lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -62,7 +62,7 @@
                    
 
 lemma JVM_states_unfold: 
-  "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*>
+  "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) \<times>
                                   list maxr (err(types S))))"
   apply (unfold states_def sl_def Opt.esl_def Err.sl_def
          stk_esl_def reg_sl_def Product.esl_def
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/MicroJava/DFA/Product.thy
--- a/src/HOL/MicroJava/DFA/Product.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/MicroJava/DFA/Product.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -16,7 +16,7 @@
 "sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)"
 
 definition esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl" where
-"esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
+"esl == %(A,rA,fA) (B,rB,fB). (A \<times> B, le rA rB, sup fA fB)"
 
 abbreviation
   lesubprod_sntax :: "'a * 'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'a * 'b \<Rightarrow> bool"
@@ -57,7 +57,7 @@
 
 lemma closed_lift2_sup:
   "\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow> 
-  closed (err(A<*>B)) (lift2(sup f g))"
+  closed (err(A\<times>B)) (lift2(sup f g))"
 apply (unfold closed_def plussub_def lift2_def err_def sup_def)
 apply (simp split: err.split)
 apply blast
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Nominal/Examples/Class3.thy
--- a/src/HOL/Nominal/Examples/Class3.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Nominal/Examples/Class3.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -2265,7 +2265,7 @@
 by (induct rule: SNa.induct) (blast)
 
 lemma wf_SNa_restricted:
-  shows "wf (A_Redu_set \<inter> (UNIV <*> SNa_set))"
+  shows "wf (A_Redu_set \<inter> (UNIV \<times> SNa_set))"
 apply(unfold wf_def)
 apply(intro strip)
 apply(case_tac "SNa x")
@@ -2280,7 +2280,7 @@
 done
 
 definition SNa_Redu :: "(trm \<times> trm) set" where
-  "SNa_Redu \<equiv> A_Redu_set \<inter> (UNIV <*> SNa_set)"
+  "SNa_Redu \<equiv> A_Redu_set \<inter> (UNIV \<times> SNa_set)"
 
 lemma wf_SNa_Redu:
   shows "wf SNa_Redu"
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -173,7 +173,7 @@
   where "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
   
 definition S :: "(int * int) set"
-  where "S = P_set <*> Q_set"
+  where "S = P_set \<times> Q_set"
 
 definition S1 :: "(int * int) set"
   where "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Product_Type.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -1005,12 +1005,8 @@
   Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
 
 abbreviation
-  Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"
-    (infixr "<*>" 80) where
-  "A <*> B == Sigma A (%_. B)"
-
-notation (xsymbols)
-  Times  (infixr "\<times>" 80)
+  Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  (infixr "\<times>" 80) where
+  "A \<times> B == Sigma A (%_. B)"
 
 hide_const (open) Times
 
@@ -1057,16 +1053,16 @@
 lemma Sigma_empty1 [simp]: "Sigma {} B = {}"
   by blast
 
-lemma Sigma_empty2 [simp]: "A <*> {} = {}"
+lemma Sigma_empty2 [simp]: "A \<times> {} = {}"
   by blast
 
-lemma UNIV_Times_UNIV [simp]: "UNIV <*> UNIV = UNIV"
+lemma UNIV_Times_UNIV [simp]: "UNIV \<times> UNIV = UNIV"
   by auto
 
-lemma Compl_Times_UNIV1 [simp]: "- (UNIV <*> A) = UNIV <*> (-A)"
+lemma Compl_Times_UNIV1 [simp]: "- (UNIV \<times> A) = UNIV \<times> (-A)"
   by auto
 
-lemma Compl_Times_UNIV2 [simp]: "- (A <*> UNIV) = (-A) <*> UNIV"
+lemma Compl_Times_UNIV2 [simp]: "- (A \<times> UNIV) = (-A) \<times> UNIV"
   by auto
 
 lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))"
@@ -1075,10 +1071,10 @@
 lemma Sigma_empty_iff: "(SIGMA i:I. X i) = {} \<longleftrightarrow> (\<forall>i\<in>I. X i = {})"
   by auto
 
-lemma Times_subset_cancel2: "x:C ==> (A <*> C <= B <*> C) = (A <= B)"
+lemma Times_subset_cancel2: "x:C ==> (A \<times> C <= B \<times> C) = (A <= B)"
   by blast
 
-lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)"
+lemma Times_eq_cancel2: "x:C ==> (A \<times> C = B \<times> C) = (A = B)"
   by (blast elim: equalityE)
 
 lemma Collect_case_prod_Sigma:
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/UNITY/Comp/TimerArray.thy
--- a/src/HOL/UNITY/Comp/TimerArray.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/UNITY/Comp/TimerArray.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -42,7 +42,7 @@
 lemma TimerArray_leadsTo_zero:
      "finite I  
       ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"
-apply (erule_tac A'1 = "%i. lift_set i ({0} <*> UNIV)" 
+apply (erule_tac A'1 = "%i. lift_set i ({0} \<times> UNIV)" 
        in finite_stable_completion [THEN leadsTo_weaken])
 apply auto
 (*Safety property, already reduced to the single Timer case*)
@@ -51,7 +51,7 @@
 (*Progress property for the array of Timers*)
 apply (rule_tac f = "sub i o fst" in lessThan_induct)
 apply (case_tac "m")
-(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
+(*Annoying need to massage the conditions to have the form (... \<times> UNIV)*)
 apply (auto intro: subset_imp_leadsTo 
         simp add: insert_absorb 
                   lift_set_Un_distrib [symmetric] lessThan_Suc [symmetric] 
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/UNITY/Extend.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -14,7 +14,7 @@
 definition
   (*MOVE to Relation.thy?*)
   Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
-  where "Restrict A r = r \<inter> (A <*> UNIV)"
+  where "Restrict A r = r \<inter> (A \<times> UNIV)"
 
 definition
   good_map :: "['a*'b => 'c] => bool"
@@ -23,7 +23,7 @@
   
 definition
   extend_set :: "['a*'b => 'c, 'a set] => 'c set"
-  where "extend_set h A = h ` (A <*> UNIV)"
+  where "extend_set h A = h ` (A \<times> UNIV)"
 
 definition
   project_set :: "['a*'b => 'c, 'c set] => 'a set"
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -270,13 +270,13 @@
      "[| delete_map j g = delete_map j g';  i\<noteq>j |] ==> g i = g' i"
 by force
 
-(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
+(*A set of the form (A \<times> UNIV) ignores the second (dummy) state component*)
 
-lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) <*> UNIV"
+lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) \<times> UNIV"
 by auto
 
 lemma vimage_sub_eq_lift_set [simp]:
-     "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)"
+     "(sub i -`A) \<times> UNIV = lift_set i (A \<times> UNIV)"
 by auto
 
 lemma mem_lift_act_iff [iff]: 
@@ -288,7 +288,7 @@
 
 lemma preserves_snd_lift_stable:
      "[| F \<in> preserves snd;  i\<noteq>j |]  
-      ==> lift j F \<in> stable (lift_set i (A <*> UNIV))"
+      ==> lift j F \<in> stable (lift_set i (A \<times> UNIV))"
 apply (auto simp add: lift_def lift_set_def stable_def constrains_def 
                       rename_def extend_def mem_rename_set_iff)
 apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
@@ -298,9 +298,9 @@
 (*If i\<noteq>j then lift j F  does nothing to lift_set i, and the 
   premise ensures A \<subseteq> B.*)
 lemma constrains_imp_lift_constrains:
-    "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);   
+    "[| F i \<in> (A \<times> UNIV) co (B \<times> UNIV);   
         F j \<in> preserves snd |]   
-     ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
+     ==> lift j (F j) \<in> (lift_set i (A \<times> UNIV)) co (lift_set i (B \<times> UNIV))"
 apply (cases "i=j")
 apply (simp add: lift_def lift_set_def rename_constrains)
 apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
@@ -310,8 +310,8 @@
 
 (*USELESS??*)
 lemma lift_map_image_Times:
-     "lift_map i ` (A <*> UNIV) =  
-      (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) <*> UNIV"
+     "lift_map i ` (A \<times> UNIV) =  
+      (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) \<times> UNIV"
 apply (auto intro!: bexI image_eqI simp add: lift_map_def)
 apply (rule split_conv [symmetric])
 done
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/UNITY/PPROD.thy
--- a/src/HOL/UNITY/PPROD.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/UNITY/PPROD.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -48,9 +48,9 @@
 
 lemma PLam_constrains:
      "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
-      ==> (PLam I F \<in> (lift_set i (A <*> UNIV)) co
-                      (lift_set i (B <*> UNIV)))  =
-          (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
+      ==> (PLam I F \<in> (lift_set i (A \<times> UNIV)) co
+                      (lift_set i (B \<times> UNIV)))  =
+          (F i \<in> (A \<times> UNIV) co (B \<times> UNIV))"
 apply (simp add: PLam_def JN_constrains)
 apply (subst insert_Diff [symmetric], assumption)
 apply (simp add: lift_constrains)
@@ -59,8 +59,8 @@
 
 lemma PLam_stable:
      "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
-      ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =
-          (F i \<in> stable (A <*> UNIV))"
+      ==> (PLam I F \<in> stable (lift_set i (A \<times> UNIV))) =
+          (F i \<in> stable (A \<times> UNIV))"
 by (simp add: stable_def PLam_constrains)
 
 lemma PLam_transient:
@@ -70,9 +70,9 @@
 
 text{*This holds because the @{term "F j"} cannot change @{term "lift_set i"}*}
 lemma PLam_ensures:
-     "[| i \<in> I;  F i \<in> (A <*> UNIV) ensures (B <*> UNIV);
+     "[| i \<in> I;  F i \<in> (A \<times> UNIV) ensures (B \<times> UNIV);
          \<forall>j. F j \<in> preserves snd |]
-      ==> PLam I F \<in> lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
+      ==> PLam I F \<in> lift_set i (A \<times> UNIV) ensures lift_set i (B \<times> UNIV)"
 apply (simp add: ensures_def PLam_constrains PLam_transient
               lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric]
               Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
@@ -82,11 +82,11 @@
 
 lemma PLam_leadsTo_Basis:
      "[| i \<in> I;
-         F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co
-               ((A <*> UNIV) \<union> (B <*> UNIV));
-         F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));
+         F i \<in> ((A \<times> UNIV) - (B \<times> UNIV)) co
+               ((A \<times> UNIV) \<union> (B \<times> UNIV));
+         F i \<in> transient ((A \<times> UNIV) - (B \<times> UNIV));
          \<forall>j. F j \<in> preserves snd |]
-      ==> PLam I F \<in> lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
+      ==> PLam I F \<in> lift_set i (A \<times> UNIV) leadsTo lift_set i (B \<times> UNIV)"
 by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
 
 
@@ -94,9 +94,9 @@
 (** invariant **)
 
 lemma invariant_imp_PLam_invariant:
-     "[| F i \<in> invariant (A <*> UNIV);  i \<in> I;
+     "[| F i \<in> invariant (A \<times> UNIV);  i \<in> I;
          \<forall>j. F j \<in> preserves snd |]
-      ==> PLam I F \<in> invariant (lift_set i (A <*> UNIV))"
+      ==> PLam I F \<in> invariant (lift_set i (A \<times> UNIV))"
 by (auto simp add: PLam_stable invariant_def)
 
 
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Wellfounded.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -32,7 +32,7 @@
 text\<open>Restriction to domain @{term A} and range @{term B}.  If @{term r} is
     well-founded over their intersection, then @{term "wf r"}\<close>
 lemma wfI: 
- "[| r \<subseteq> A <*> B; 
+ "[| r \<subseteq> A \<times> B; 
      !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]
   ==>  wf r"
   unfolding wf_def by blast