discontinued ASCII replacement syntax <*>;
authorwenzelm
Sun Dec 27 22:07:17 2015 +0100 (2015-12-27)
changeset 619437fba644ed827
parent 61942 f02b26f7d39d
child 61944 5d06ecfdb472
discontinued ASCII replacement syntax <*>;
NEWS
src/Doc/Main/Main_Doc.thy
src/HOL/BNF_Cardinal_Arithmetic.thy
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/BNF_Greatest_Fixpoint.thy
src/HOL/BNF_Wellorder_Constructions.thy
src/HOL/Cardinals/Cardinal_Arithmetic.thy
src/HOL/Cardinals/Cardinal_Order_Relation.thy
src/HOL/Groups_Big.thy
src/HOL/Induct/SList.thy
src/HOL/Induct/Sexp.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Old_Datatype.thy
src/HOL/MicroJava/BV/JVMType.thy
src/HOL/MicroJava/DFA/Product.thy
src/HOL/Nominal/Examples/Class3.thy
src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Product_Type.thy
src/HOL/UNITY/Comp/TimerArray.thy
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/PPROD.thy
src/HOL/Wellfounded.thy
     1.1 --- a/NEWS	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/NEWS	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -476,6 +476,8 @@
     1.4  
     1.5    notation iff  (infixr "<->" 25)
     1.6  
     1.7 +  notation Times  (infixr "<*>" 80)
     1.8 +
     1.9    type_notation Map.map  (infixr "~=>" 0)
    1.10    notation Map.map_comp  (infixl "o'_m" 55)
    1.11  
     2.1 --- a/src/Doc/Main/Main_Doc.thy	Sun Dec 27 21:46:36 2015 +0100
     2.2 +++ b/src/Doc/Main/Main_Doc.thy	Sun Dec 27 22:07:17 2015 +0100
     2.3 @@ -228,7 +228,7 @@
     2.4  \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
     2.5  @{term"Pair a b"} & @{term[source]"Pair a b"}\\
     2.6  @{term"case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
     2.7 -@{term"A <*> B"} &  @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$)
     2.8 +@{term"A \<times> B"} &  @{text"Sigma A (\<lambda>\<^raw:\_>. B)"}
     2.9  \end{tabular}
    2.10  
    2.11  Pairs may be nested. Nesting to the right is printed as a tuple,
     3.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Sun Dec 27 21:46:36 2015 +0100
     3.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Sun Dec 27 22:07:17 2015 +0100
     3.3 @@ -281,7 +281,7 @@
     3.4  subsection \<open>Product\<close>
     3.5  
     3.6  definition cprod (infixr "*c" 80) where
     3.7 -  "r1 *c r2 = |Field r1 <*> Field r2|"
     3.8 +  "r1 *c r2 = |Field r1 \<times> Field r2|"
     3.9  
    3.10  lemma card_order_cprod:
    3.11    assumes "card_order r1" "card_order r2"
     4.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Dec 27 21:46:36 2015 +0100
     4.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Sun Dec 27 22:07:17 2015 +0100
     4.3 @@ -788,7 +788,7 @@
     4.4  qed
     4.5  
     4.6  lemma card_of_Times_Plus_distrib:
     4.7 -  "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|")
     4.8 +  "|A \<times> (B <+> C)| =o |A \<times> B <+> A \<times> C|" (is "|?RHS| =o |?LHS|")
     4.9  proof -
    4.10    let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
    4.11    have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force
    4.12 @@ -1038,7 +1038,7 @@
    4.13  
    4.14  lemma card_of_Times_ordLeq_infinite_Field:
    4.15  "\<lbrakk>\<not>finite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
    4.16 - \<Longrightarrow> |A <*> B| \<le>o r"
    4.17 + \<Longrightarrow> |A \<times> B| \<le>o r"
    4.18  by(simp add: card_of_Sigma_ordLeq_infinite_Field)
    4.19  
    4.20  lemma card_of_Times_infinite_simps:
    4.21 @@ -1619,7 +1619,7 @@
    4.22  subsection \<open>Others\<close>
    4.23  
    4.24  lemma card_of_Func_Times:
    4.25 -"|Func (A <*> B) C| =o |Func A (Func B C)|"
    4.26 +"|Func (A \<times> B) C| =o |Func A (Func B C)|"
    4.27  unfolding card_of_ordIso[symmetric]
    4.28  using bij_betw_curr by blast
    4.29  
    4.30 @@ -1661,7 +1661,7 @@
    4.31  qed
    4.32  
    4.33  lemma Func_Times_Range:
    4.34 -  "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|")
    4.35 +  "|Func A (B \<times> C)| =o |Func A B \<times> Func A C|" (is "|?LHS| =o |?RHS|")
    4.36  proof -
    4.37    let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined,
    4.38                    \<lambda>x. if x \<in> A then snd (fg x) else undefined)"
     5.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Dec 27 21:46:36 2015 +0100
     5.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Dec 27 22:07:17 2015 +0100
     5.3 @@ -73,7 +73,7 @@
     5.4  lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
     5.5    unfolding Gr_def by simp
     5.6  
     5.7 -lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
     5.8 +lemma Gr_incl: "Gr A f \<subseteq> A \<times> B \<longleftrightarrow> f ` A \<subseteq> B"
     5.9    unfolding Gr_def by auto
    5.10  
    5.11  lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
    5.12 @@ -137,7 +137,7 @@
    5.13    by (auto simp: proj_preserves)
    5.14  
    5.15  lemma relImage_relInvImage:
    5.16 -  assumes "R \<subseteq> f ` A <*> f ` A"
    5.17 +  assumes "R \<subseteq> f ` A \<times> f ` A"
    5.18    shows "relImage (relInvImage A R f) f = R"
    5.19    using assms unfolding relImage_def relInvImage_def by fast
    5.20  
     6.1 --- a/src/HOL/BNF_Wellorder_Constructions.thy	Sun Dec 27 21:46:36 2015 +0100
     6.2 +++ b/src/HOL/BNF_Wellorder_Constructions.thy	Sun Dec 27 22:07:17 2015 +0100
     6.3 @@ -1515,19 +1515,19 @@
     6.4  "curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
     6.5  
     6.6  lemma curr_in:
     6.7 -assumes f: "f \<in> Func (A <*> B) C"
     6.8 +assumes f: "f \<in> Func (A \<times> B) C"
     6.9  shows "curr A f \<in> Func A (Func B C)"
    6.10  using assms unfolding curr_def Func_def by auto
    6.11  
    6.12  lemma curr_inj:
    6.13 -assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C"
    6.14 +assumes "f1 \<in> Func (A \<times> B) C" and "f2 \<in> Func (A \<times> B) C"
    6.15  shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
    6.16  proof safe
    6.17    assume c: "curr A f1 = curr A f2"
    6.18    show "f1 = f2"
    6.19    proof (rule ext, clarify)
    6.20      fix a b show "f1 (a, b) = f2 (a, b)"
    6.21 -    proof (cases "(a,b) \<in> A <*> B")
    6.22 +    proof (cases "(a,b) \<in> A \<times> B")
    6.23        case False
    6.24        thus ?thesis using assms unfolding Func_def by auto
    6.25      next
    6.26 @@ -1540,7 +1540,7 @@
    6.27  
    6.28  lemma curr_surj:
    6.29  assumes "g \<in> Func A (Func B C)"
    6.30 -shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g"
    6.31 +shows "\<exists> f \<in> Func (A \<times> B) C. curr A f = g"
    6.32  proof
    6.33    let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"
    6.34    show "curr A ?f = g"
    6.35 @@ -1557,11 +1557,11 @@
    6.36        thus ?thesis using True unfolding Func_def curr_def by auto
    6.37      qed
    6.38    qed
    6.39 -  show "?f \<in> Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto
    6.40 +  show "?f \<in> Func (A \<times> B) C" using assms unfolding Func_def mem_Collect_eq by auto
    6.41  qed
    6.42  
    6.43  lemma bij_betw_curr:
    6.44 -"bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))"
    6.45 +"bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))"
    6.46  unfolding bij_betw_def inj_on_def image_def
    6.47  apply (intro impI conjI ballI)
    6.48  apply (erule curr_inj[THEN iffD1], assumption+)
     7.1 --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Sun Dec 27 21:46:36 2015 +0100
     7.2 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Sun Dec 27 22:07:17 2015 +0100
     7.3 @@ -51,8 +51,8 @@
     7.4  shows "|A \<times> {x}| =o |A|"
     7.5  proof -
     7.6    def f \<equiv> "\<lambda>(a::'a,b::'b). (a)"
     7.7 -  have "A \<subseteq> f ` (A <*> {x})" unfolding f_def by (auto simp: image_iff)
     7.8 -  hence "bij_betw f (A <*> {x}) A"  unfolding bij_betw_def inj_on_def f_def by fastforce
     7.9 +  have "A \<subseteq> f ` (A \<times> {x})" unfolding f_def by (auto simp: image_iff)
    7.10 +  hence "bij_betw f (A \<times> {x}) A"  unfolding bij_betw_def inj_on_def f_def by fastforce
    7.11    thus ?thesis using card_of_ordIso by blast
    7.12  qed
    7.13  
     8.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Sun Dec 27 21:46:36 2015 +0100
     8.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Sun Dec 27 22:07:17 2015 +0100
     8.3 @@ -489,7 +489,7 @@
     8.4  
     8.5  lemma card_of_Times_ordLeq_infinite:
     8.6  "\<lbrakk>\<not>finite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
     8.7 - \<Longrightarrow> |A <*> B| \<le>o |C|"
     8.8 + \<Longrightarrow> |A \<times> B| \<le>o |C|"
     8.9  by(simp add: card_of_Sigma_ordLeq_infinite)
    8.10  
    8.11  corollary Plus_infinite_bij_betw:
    8.12 @@ -621,7 +621,7 @@
    8.13    ordIso_symmetric by blast
    8.14    hence "|A| <o |?C|"  "|B| <o |?C|"
    8.15    using LESS1 LESS2 ordLess_ordIso_trans by blast+
    8.16 -  hence  "|A <*> B| <o |?C|" using INF
    8.17 +  hence  "|A \<times> B| <o |?C|" using INF
    8.18    card_of_Times_ordLess_infinite by blast
    8.19    thus ?thesis using 1 ordLess_ordIso_trans by blast
    8.20  qed
    8.21 @@ -1502,12 +1502,12 @@
    8.22  
    8.23  lemma card_of_Pfunc_Pow_Func_option:
    8.24  assumes "B \<noteq> {}"
    8.25 -shows "|Pfunc A B| \<le>o |Pow A <*> Func_option A B|"
    8.26 +shows "|Pfunc A B| \<le>o |Pow A \<times> Func_option A B|"
    8.27  proof-
    8.28    have "|Pfunc A B| =o |\<Union>A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
    8.29      unfolding Pfunc_Func_option by(rule card_of_refl)
    8.30    also have "?K \<le>o |Sigma (Pow A) (\<lambda> A'. Func_option A' B)|" using card_of_UNION_Sigma .
    8.31 -  also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A <*> Func_option A B|"
    8.32 +  also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A \<times> Func_option A B|"
    8.33      apply(rule card_of_Sigma_mono1) using card_of_Func_option_mono[OF _ assms] by auto
    8.34    finally show ?thesis .
    8.35  qed
     9.1 --- a/src/HOL/Groups_Big.thy	Sun Dec 27 21:46:36 2015 +0100
     9.2 +++ b/src/HOL/Groups_Big.thy	Sun Dec 27 22:07:17 2015 +0100
     9.3 @@ -350,7 +350,7 @@
     9.4  qed
     9.5  
     9.6  lemma cartesian_product:
     9.7 -   "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A <*> B)"
     9.8 +   "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A \<times> B)"
     9.9  apply (rule sym)
    9.10  apply (cases "finite A") 
    9.11   apply (cases "finite B") 
    9.12 @@ -1032,15 +1032,15 @@
    9.13  
    9.14  (*
    9.15  lemma SigmaI_insert: "y \<notin> A ==>
    9.16 -  (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
    9.17 +  (SIGMA x:(insert y A). B x) = (({y} \<times> (B y)) \<union> (SIGMA x: A. B x))"
    9.18    by auto
    9.19  *)
    9.20  
    9.21 -lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
    9.22 +lemma card_cartesian_product: "card (A \<times> B) = card(A) * card(B)"
    9.23    by (cases "finite A \<and> finite B")
    9.24      (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
    9.25  
    9.26 -lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
    9.27 +lemma card_cartesian_product_singleton:  "card({x} \<times> A) = card(A)"
    9.28  by (simp add: card_cartesian_product)
    9.29  
    9.30  
    10.1 --- a/src/HOL/Induct/SList.thy	Sun Dec 27 21:46:36 2015 +0100
    10.2 +++ b/src/HOL/Induct/SList.thy	Sun Dec 27 22:07:17 2015 +0100
    10.3 @@ -10,8 +10,8 @@
    10.4  
    10.5  Definition of type 'a list (strict lists) by a least fixed point
    10.6  
    10.7 -We use          list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
    10.8 -and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
    10.9 +We use          list(A) == lfp(%Z. {NUMB(0)} <+> A \<times> Z)
   10.10 +and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) \<times> Z)
   10.11  
   10.12  so that list can serve as a "functor" for defining other recursive types.
   10.13  
    11.1 --- a/src/HOL/Induct/Sexp.thy	Sun Dec 27 21:46:36 2015 +0100
    11.2 +++ b/src/HOL/Induct/Sexp.thy	Sun Dec 27 22:07:17 2015 +0100
    11.3 @@ -74,7 +74,7 @@
    11.4  
    11.5  (** Introduction rules for 'pred_sexp' **)
    11.6  
    11.7 -lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp"
    11.8 +lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp \<times> sexp"
    11.9    by (simp add: pred_sexp_def) blast
   11.10  
   11.11  (* (a,b) \<in> pred_sexp^+ ==> a \<in> sexp *)
    12.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sun Dec 27 21:46:36 2015 +0100
    12.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Dec 27 22:07:17 2015 +0100
    12.3 @@ -3108,7 +3108,7 @@
    12.4      setsum (\<lambda>(k,m). a$k * b$m * (c^k * d^m) $ n) {(k,m). k + m \<le> n}"  (is "?l = ?r")
    12.5  proof -
    12.6    let ?S = "{(k::nat, m::nat). k + m \<le> n}"
    12.7 -  have s: "?S \<subseteq> {0..n} <*> {0..n}" by (auto simp add: subset_eq)
    12.8 +  have s: "?S \<subseteq> {0..n} \<times> {0..n}" by (auto simp add: subset_eq)
    12.9    have f: "finite {(k::nat, m::nat). k + m \<le> n}"
   12.10      apply (rule finite_subset[OF s])
   12.11      apply auto
    13.1 --- a/src/HOL/Library/Old_Datatype.thy	Sun Dec 27 21:46:36 2015 +0100
    13.2 +++ b/src/HOL/Library/Old_Datatype.thy	Sun Dec 27 22:07:17 2015 +0100
    13.3 @@ -495,7 +495,7 @@
    13.4  
    13.5  (*** Bounding theorems ***)
    13.6  
    13.7 -lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"
    13.8 +lemma dprod_Sigma: "(dprod (A \<times> B) (C \<times> D)) <= (uprod A C) \<times> (uprod B D)"
    13.9  by blast
   13.10  
   13.11  lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma]
   13.12 @@ -505,7 +505,7 @@
   13.13      "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
   13.14  by auto
   13.15  
   13.16 -lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"
   13.17 +lemma dsum_Sigma: "(dsum (A \<times> B) (C \<times> D)) <= (usum A C) \<times> (usum B D)"
   13.18  by blast
   13.19  
   13.20  lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
    14.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Sun Dec 27 21:46:36 2015 +0100
    14.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Sun Dec 27 22:07:17 2015 +0100
    14.3 @@ -62,7 +62,7 @@
    14.4                     
    14.5  
    14.6  lemma JVM_states_unfold: 
    14.7 -  "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*>
    14.8 +  "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) \<times>
    14.9                                    list maxr (err(types S))))"
   14.10    apply (unfold states_def sl_def Opt.esl_def Err.sl_def
   14.11           stk_esl_def reg_sl_def Product.esl_def
    15.1 --- a/src/HOL/MicroJava/DFA/Product.thy	Sun Dec 27 21:46:36 2015 +0100
    15.2 +++ b/src/HOL/MicroJava/DFA/Product.thy	Sun Dec 27 22:07:17 2015 +0100
    15.3 @@ -16,7 +16,7 @@
    15.4  "sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)"
    15.5  
    15.6  definition esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl" where
    15.7 -"esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
    15.8 +"esl == %(A,rA,fA) (B,rB,fB). (A \<times> B, le rA rB, sup fA fB)"
    15.9  
   15.10  abbreviation
   15.11    lesubprod_sntax :: "'a * 'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   15.12 @@ -57,7 +57,7 @@
   15.13  
   15.14  lemma closed_lift2_sup:
   15.15    "\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow> 
   15.16 -  closed (err(A<*>B)) (lift2(sup f g))"
   15.17 +  closed (err(A\<times>B)) (lift2(sup f g))"
   15.18  apply (unfold closed_def plussub_def lift2_def err_def sup_def)
   15.19  apply (simp split: err.split)
   15.20  apply blast
    16.1 --- a/src/HOL/Nominal/Examples/Class3.thy	Sun Dec 27 21:46:36 2015 +0100
    16.2 +++ b/src/HOL/Nominal/Examples/Class3.thy	Sun Dec 27 22:07:17 2015 +0100
    16.3 @@ -2265,7 +2265,7 @@
    16.4  by (induct rule: SNa.induct) (blast)
    16.5  
    16.6  lemma wf_SNa_restricted:
    16.7 -  shows "wf (A_Redu_set \<inter> (UNIV <*> SNa_set))"
    16.8 +  shows "wf (A_Redu_set \<inter> (UNIV \<times> SNa_set))"
    16.9  apply(unfold wf_def)
   16.10  apply(intro strip)
   16.11  apply(case_tac "SNa x")
   16.12 @@ -2280,7 +2280,7 @@
   16.13  done
   16.14  
   16.15  definition SNa_Redu :: "(trm \<times> trm) set" where
   16.16 -  "SNa_Redu \<equiv> A_Redu_set \<inter> (UNIV <*> SNa_set)"
   16.17 +  "SNa_Redu \<equiv> A_Redu_set \<inter> (UNIV \<times> SNa_set)"
   16.18  
   16.19  lemma wf_SNa_Redu:
   16.20    shows "wf SNa_Redu"
    17.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Dec 27 21:46:36 2015 +0100
    17.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Dec 27 22:07:17 2015 +0100
    17.3 @@ -173,7 +173,7 @@
    17.4    where "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
    17.5    
    17.6  definition S :: "(int * int) set"
    17.7 -  where "S = P_set <*> Q_set"
    17.8 +  where "S = P_set \<times> Q_set"
    17.9  
   17.10  definition S1 :: "(int * int) set"
   17.11    where "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
    18.1 --- a/src/HOL/Product_Type.thy	Sun Dec 27 21:46:36 2015 +0100
    18.2 +++ b/src/HOL/Product_Type.thy	Sun Dec 27 22:07:17 2015 +0100
    18.3 @@ -1005,12 +1005,8 @@
    18.4    Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
    18.5  
    18.6  abbreviation
    18.7 -  Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"
    18.8 -    (infixr "<*>" 80) where
    18.9 -  "A <*> B == Sigma A (%_. B)"
   18.10 -
   18.11 -notation (xsymbols)
   18.12 -  Times  (infixr "\<times>" 80)
   18.13 +  Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  (infixr "\<times>" 80) where
   18.14 +  "A \<times> B == Sigma A (%_. B)"
   18.15  
   18.16  hide_const (open) Times
   18.17  
   18.18 @@ -1057,16 +1053,16 @@
   18.19  lemma Sigma_empty1 [simp]: "Sigma {} B = {}"
   18.20    by blast
   18.21  
   18.22 -lemma Sigma_empty2 [simp]: "A <*> {} = {}"
   18.23 +lemma Sigma_empty2 [simp]: "A \<times> {} = {}"
   18.24    by blast
   18.25  
   18.26 -lemma UNIV_Times_UNIV [simp]: "UNIV <*> UNIV = UNIV"
   18.27 +lemma UNIV_Times_UNIV [simp]: "UNIV \<times> UNIV = UNIV"
   18.28    by auto
   18.29  
   18.30 -lemma Compl_Times_UNIV1 [simp]: "- (UNIV <*> A) = UNIV <*> (-A)"
   18.31 +lemma Compl_Times_UNIV1 [simp]: "- (UNIV \<times> A) = UNIV \<times> (-A)"
   18.32    by auto
   18.33  
   18.34 -lemma Compl_Times_UNIV2 [simp]: "- (A <*> UNIV) = (-A) <*> UNIV"
   18.35 +lemma Compl_Times_UNIV2 [simp]: "- (A \<times> UNIV) = (-A) \<times> UNIV"
   18.36    by auto
   18.37  
   18.38  lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))"
   18.39 @@ -1075,10 +1071,10 @@
   18.40  lemma Sigma_empty_iff: "(SIGMA i:I. X i) = {} \<longleftrightarrow> (\<forall>i\<in>I. X i = {})"
   18.41    by auto
   18.42  
   18.43 -lemma Times_subset_cancel2: "x:C ==> (A <*> C <= B <*> C) = (A <= B)"
   18.44 +lemma Times_subset_cancel2: "x:C ==> (A \<times> C <= B \<times> C) = (A <= B)"
   18.45    by blast
   18.46  
   18.47 -lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)"
   18.48 +lemma Times_eq_cancel2: "x:C ==> (A \<times> C = B \<times> C) = (A = B)"
   18.49    by (blast elim: equalityE)
   18.50  
   18.51  lemma Collect_case_prod_Sigma:
    19.1 --- a/src/HOL/UNITY/Comp/TimerArray.thy	Sun Dec 27 21:46:36 2015 +0100
    19.2 +++ b/src/HOL/UNITY/Comp/TimerArray.thy	Sun Dec 27 22:07:17 2015 +0100
    19.3 @@ -42,7 +42,7 @@
    19.4  lemma TimerArray_leadsTo_zero:
    19.5       "finite I  
    19.6        ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"
    19.7 -apply (erule_tac A'1 = "%i. lift_set i ({0} <*> UNIV)" 
    19.8 +apply (erule_tac A'1 = "%i. lift_set i ({0} \<times> UNIV)" 
    19.9         in finite_stable_completion [THEN leadsTo_weaken])
   19.10  apply auto
   19.11  (*Safety property, already reduced to the single Timer case*)
   19.12 @@ -51,7 +51,7 @@
   19.13  (*Progress property for the array of Timers*)
   19.14  apply (rule_tac f = "sub i o fst" in lessThan_induct)
   19.15  apply (case_tac "m")
   19.16 -(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
   19.17 +(*Annoying need to massage the conditions to have the form (... \<times> UNIV)*)
   19.18  apply (auto intro: subset_imp_leadsTo 
   19.19          simp add: insert_absorb 
   19.20                    lift_set_Un_distrib [symmetric] lessThan_Suc [symmetric] 
    20.1 --- a/src/HOL/UNITY/Extend.thy	Sun Dec 27 21:46:36 2015 +0100
    20.2 +++ b/src/HOL/UNITY/Extend.thy	Sun Dec 27 22:07:17 2015 +0100
    20.3 @@ -14,7 +14,7 @@
    20.4  definition
    20.5    (*MOVE to Relation.thy?*)
    20.6    Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
    20.7 -  where "Restrict A r = r \<inter> (A <*> UNIV)"
    20.8 +  where "Restrict A r = r \<inter> (A \<times> UNIV)"
    20.9  
   20.10  definition
   20.11    good_map :: "['a*'b => 'c] => bool"
   20.12 @@ -23,7 +23,7 @@
   20.13    
   20.14  definition
   20.15    extend_set :: "['a*'b => 'c, 'a set] => 'c set"
   20.16 -  where "extend_set h A = h ` (A <*> UNIV)"
   20.17 +  where "extend_set h A = h ` (A \<times> UNIV)"
   20.18  
   20.19  definition
   20.20    project_set :: "['a*'b => 'c, 'c set] => 'a set"
    21.1 --- a/src/HOL/UNITY/Lift_prog.thy	Sun Dec 27 21:46:36 2015 +0100
    21.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Sun Dec 27 22:07:17 2015 +0100
    21.3 @@ -270,13 +270,13 @@
    21.4       "[| delete_map j g = delete_map j g';  i\<noteq>j |] ==> g i = g' i"
    21.5  by force
    21.6  
    21.7 -(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
    21.8 +(*A set of the form (A \<times> UNIV) ignores the second (dummy) state component*)
    21.9  
   21.10 -lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) <*> UNIV"
   21.11 +lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) \<times> UNIV"
   21.12  by auto
   21.13  
   21.14  lemma vimage_sub_eq_lift_set [simp]:
   21.15 -     "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)"
   21.16 +     "(sub i -`A) \<times> UNIV = lift_set i (A \<times> UNIV)"
   21.17  by auto
   21.18  
   21.19  lemma mem_lift_act_iff [iff]: 
   21.20 @@ -288,7 +288,7 @@
   21.21  
   21.22  lemma preserves_snd_lift_stable:
   21.23       "[| F \<in> preserves snd;  i\<noteq>j |]  
   21.24 -      ==> lift j F \<in> stable (lift_set i (A <*> UNIV))"
   21.25 +      ==> lift j F \<in> stable (lift_set i (A \<times> UNIV))"
   21.26  apply (auto simp add: lift_def lift_set_def stable_def constrains_def 
   21.27                        rename_def extend_def mem_rename_set_iff)
   21.28  apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
   21.29 @@ -298,9 +298,9 @@
   21.30  (*If i\<noteq>j then lift j F  does nothing to lift_set i, and the 
   21.31    premise ensures A \<subseteq> B.*)
   21.32  lemma constrains_imp_lift_constrains:
   21.33 -    "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);   
   21.34 +    "[| F i \<in> (A \<times> UNIV) co (B \<times> UNIV);   
   21.35          F j \<in> preserves snd |]   
   21.36 -     ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
   21.37 +     ==> lift j (F j) \<in> (lift_set i (A \<times> UNIV)) co (lift_set i (B \<times> UNIV))"
   21.38  apply (cases "i=j")
   21.39  apply (simp add: lift_def lift_set_def rename_constrains)
   21.40  apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
   21.41 @@ -310,8 +310,8 @@
   21.42  
   21.43  (*USELESS??*)
   21.44  lemma lift_map_image_Times:
   21.45 -     "lift_map i ` (A <*> UNIV) =  
   21.46 -      (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) <*> UNIV"
   21.47 +     "lift_map i ` (A \<times> UNIV) =  
   21.48 +      (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) \<times> UNIV"
   21.49  apply (auto intro!: bexI image_eqI simp add: lift_map_def)
   21.50  apply (rule split_conv [symmetric])
   21.51  done
    22.1 --- a/src/HOL/UNITY/PPROD.thy	Sun Dec 27 21:46:36 2015 +0100
    22.2 +++ b/src/HOL/UNITY/PPROD.thy	Sun Dec 27 22:07:17 2015 +0100
    22.3 @@ -48,9 +48,9 @@
    22.4  
    22.5  lemma PLam_constrains:
    22.6       "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
    22.7 -      ==> (PLam I F \<in> (lift_set i (A <*> UNIV)) co
    22.8 -                      (lift_set i (B <*> UNIV)))  =
    22.9 -          (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
   22.10 +      ==> (PLam I F \<in> (lift_set i (A \<times> UNIV)) co
   22.11 +                      (lift_set i (B \<times> UNIV)))  =
   22.12 +          (F i \<in> (A \<times> UNIV) co (B \<times> UNIV))"
   22.13  apply (simp add: PLam_def JN_constrains)
   22.14  apply (subst insert_Diff [symmetric], assumption)
   22.15  apply (simp add: lift_constrains)
   22.16 @@ -59,8 +59,8 @@
   22.17  
   22.18  lemma PLam_stable:
   22.19       "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
   22.20 -      ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =
   22.21 -          (F i \<in> stable (A <*> UNIV))"
   22.22 +      ==> (PLam I F \<in> stable (lift_set i (A \<times> UNIV))) =
   22.23 +          (F i \<in> stable (A \<times> UNIV))"
   22.24  by (simp add: stable_def PLam_constrains)
   22.25  
   22.26  lemma PLam_transient:
   22.27 @@ -70,9 +70,9 @@
   22.28  
   22.29  text{*This holds because the @{term "F j"} cannot change @{term "lift_set i"}*}
   22.30  lemma PLam_ensures:
   22.31 -     "[| i \<in> I;  F i \<in> (A <*> UNIV) ensures (B <*> UNIV);
   22.32 +     "[| i \<in> I;  F i \<in> (A \<times> UNIV) ensures (B \<times> UNIV);
   22.33           \<forall>j. F j \<in> preserves snd |]
   22.34 -      ==> PLam I F \<in> lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
   22.35 +      ==> PLam I F \<in> lift_set i (A \<times> UNIV) ensures lift_set i (B \<times> UNIV)"
   22.36  apply (simp add: ensures_def PLam_constrains PLam_transient
   22.37                lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric]
   22.38                Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
   22.39 @@ -82,11 +82,11 @@
   22.40  
   22.41  lemma PLam_leadsTo_Basis:
   22.42       "[| i \<in> I;
   22.43 -         F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co
   22.44 -               ((A <*> UNIV) \<union> (B <*> UNIV));
   22.45 -         F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));
   22.46 +         F i \<in> ((A \<times> UNIV) - (B \<times> UNIV)) co
   22.47 +               ((A \<times> UNIV) \<union> (B \<times> UNIV));
   22.48 +         F i \<in> transient ((A \<times> UNIV) - (B \<times> UNIV));
   22.49           \<forall>j. F j \<in> preserves snd |]
   22.50 -      ==> PLam I F \<in> lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
   22.51 +      ==> PLam I F \<in> lift_set i (A \<times> UNIV) leadsTo lift_set i (B \<times> UNIV)"
   22.52  by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
   22.53  
   22.54  
   22.55 @@ -94,9 +94,9 @@
   22.56  (** invariant **)
   22.57  
   22.58  lemma invariant_imp_PLam_invariant:
   22.59 -     "[| F i \<in> invariant (A <*> UNIV);  i \<in> I;
   22.60 +     "[| F i \<in> invariant (A \<times> UNIV);  i \<in> I;
   22.61           \<forall>j. F j \<in> preserves snd |]
   22.62 -      ==> PLam I F \<in> invariant (lift_set i (A <*> UNIV))"
   22.63 +      ==> PLam I F \<in> invariant (lift_set i (A \<times> UNIV))"
   22.64  by (auto simp add: PLam_stable invariant_def)
   22.65  
   22.66  
    23.1 --- a/src/HOL/Wellfounded.thy	Sun Dec 27 21:46:36 2015 +0100
    23.2 +++ b/src/HOL/Wellfounded.thy	Sun Dec 27 22:07:17 2015 +0100
    23.3 @@ -32,7 +32,7 @@
    23.4  text\<open>Restriction to domain @{term A} and range @{term B}.  If @{term r} is
    23.5      well-founded over their intersection, then @{term "wf r"}\<close>
    23.6  lemma wfI: 
    23.7 - "[| r \<subseteq> A <*> B; 
    23.8 + "[| r \<subseteq> A \<times> B; 
    23.9       !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]
   23.10    ==>  wf r"
   23.11    unfolding wf_def by blast