"prod" and "sum" replace "*" and "+" respectively
authorhaftmann
Thu Jul 01 16:54:44 2010 +0200 (2010-07-01)
changeset 376780040bafffdef
parent 37677 c5a8b612e571
child 37679 03217132b792
"prod" and "sum" replace "*" and "+" respectively
src/HOL/Bali/Decl.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/WellForm.thy
src/HOL/Extraction/Greatest_Common_Divisor.thy
src/HOL/Extraction/Pigeonhole.thy
src/HOL/Finite_Set.thy
src/HOL/Imperative_HOL/Heap.thy
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/HOL/pair.imp
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Lambda/WeakNorm.thy
src/HOL/Lattice/Lattice.thy
src/HOL/Lattice/Orders.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Enum.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Library/Product_ord.thy
src/HOL/Library/Product_plus.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
src/HOL/TLA/Action.thy
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Function/measure_functions.ML
src/HOL/Tools/Function/sum_tree.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_rep.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/Sledgehammer/metis_clauses.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/split_rule.ML
src/HOLCF/Bifinite.thy
src/HOLCF/IOA/Modelcheck/MuIOA.thy
src/HOLCF/IOA/meta_theory/automaton.ML
src/HOLCF/Library/Sum_Cpo.thy
src/HOLCF/Product_Cpo.thy
src/HOLCF/Representable.thy
src/Pure/Isar/class_target.ML
     1.1 --- a/src/HOL/Bali/Decl.thy	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Bali/Decl.thy	Thu Jul 01 16:54:44 2010 +0200
     1.3 @@ -257,7 +257,7 @@
     1.4  lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)"
     1.5  by (cases m) (simp add: memberdecl_memberid_def)
     1.6  
     1.7 -instantiation * :: (type, has_memberid) has_memberid
     1.8 +instantiation prod :: (type, has_memberid) has_memberid
     1.9  begin
    1.10  
    1.11  definition
     2.1 --- a/src/HOL/Bali/DeclConcepts.thy	Thu Jul 01 16:54:42 2010 +0200
     2.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Thu Jul 01 16:54:44 2010 +0200
     2.3 @@ -109,7 +109,7 @@
     2.4  lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
     2.5  by (simp add: decl_acc_modi_def)
     2.6  
     2.7 -instantiation * :: (type, has_accmodi) has_accmodi
     2.8 +instantiation prod :: (type, has_accmodi) has_accmodi
     2.9  begin
    2.10  
    2.11  definition
    2.12 @@ -165,7 +165,7 @@
    2.13  lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
    2.14  by (simp add: qtname_declclass_def)
    2.15  
    2.16 -instantiation * :: (has_declclass, type) has_declclass
    2.17 +instantiation prod :: (has_declclass, type) has_declclass
    2.18  begin
    2.19  
    2.20  definition
    2.21 @@ -204,7 +204,7 @@
    2.22  lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
    2.23  by (simp add: static_field_type_is_static_def)
    2.24  
    2.25 -instantiation * :: (type, has_static) has_static
    2.26 +instantiation prod :: (type, has_static) has_static
    2.27  begin
    2.28  
    2.29  definition
    2.30 @@ -472,7 +472,7 @@
    2.31  lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
    2.32  by (simp add: mhead_def mhead_resTy_simp)
    2.33  
    2.34 -instantiation * :: ("type","has_resTy") has_resTy
    2.35 +instantiation prod :: ("type","has_resTy") has_resTy
    2.36  begin
    2.37  
    2.38  definition
     3.1 --- a/src/HOL/Bali/WellForm.thy	Thu Jul 01 16:54:42 2010 +0200
     3.2 +++ b/src/HOL/Bali/WellForm.thy	Thu Jul 01 16:54:44 2010 +0200
     3.3 @@ -2168,7 +2168,7 @@
     3.4        by (force dest!: ws_dynmethd accmethd_SomeD)
     3.5      with dynlookup eq_mheads 
     3.6      show ?thesis 
     3.7 -      by (cases emh type: *) (auto)
     3.8 +      by (cases emh type: prod) (auto)
     3.9    next
    3.10      case Iface_methd
    3.11      fix I im
    3.12 @@ -2191,7 +2191,7 @@
    3.13        by (force dest: implmt_methd)
    3.14      with dynlookup eq_mheads
    3.15      show ?thesis 
    3.16 -      by (cases emh type: *) (auto)
    3.17 +      by (cases emh type: prod) (auto)
    3.18    next
    3.19      case Iface_Object_methd
    3.20      fix I sm
    3.21 @@ -2217,7 +2217,7 @@
    3.22                    intro: class_Object [OF wf] intro: that)
    3.23         with dynlookup eq_mheads
    3.24         show ?thesis 
    3.25 -         by (cases emh type: *) (auto)
    3.26 +         by (cases emh type: prod) (auto)
    3.27       next
    3.28         case False
    3.29         with statI
    3.30 @@ -2243,7 +2243,7 @@
    3.31           by (auto dest: implmt_methd)
    3.32         with wf eq_stat resProp dynlookup eq_mheads
    3.33         show ?thesis 
    3.34 -         by (cases emh type: *) (auto intro: widen_trans)
    3.35 +         by (cases emh type: prod) (auto intro: widen_trans)
    3.36       qed
    3.37    next
    3.38      case Array_Object_methd
    3.39 @@ -2256,7 +2256,7 @@
    3.40        by (auto simp add: dynlookup_def dynmethd_C_C)
    3.41      with sm eq_mheads sm 
    3.42      show ?thesis 
    3.43 -      by (cases emh type: *) (auto dest: accmethd_SomeD)
    3.44 +      by (cases emh type: prod) (auto dest: accmethd_SomeD)
    3.45    qed
    3.46  qed
    3.47  declare split_paired_All [simp] split_paired_Ex [simp]
     4.1 --- a/src/HOL/Extraction/Greatest_Common_Divisor.thy	Thu Jul 01 16:54:42 2010 +0200
     4.2 +++ b/src/HOL/Extraction/Greatest_Common_Divisor.thy	Thu Jul 01 16:54:44 2010 +0200
     4.3 @@ -69,7 +69,7 @@
     4.4  
     4.5  end
     4.6  
     4.7 -instantiation * :: (default, default) default
     4.8 +instantiation prod :: (default, default) default
     4.9  begin
    4.10  
    4.11  definition "default = (default, default)"
     5.1 --- a/src/HOL/Extraction/Pigeonhole.thy	Thu Jul 01 16:54:42 2010 +0200
     5.2 +++ b/src/HOL/Extraction/Pigeonhole.thy	Thu Jul 01 16:54:44 2010 +0200
     5.3 @@ -227,7 +227,7 @@
     5.4  
     5.5  end
     5.6  
     5.7 -instantiation * :: (default, default) default
     5.8 +instantiation prod :: (default, default) default
     5.9  begin
    5.10  
    5.11  definition "default = (default, default)"
     6.1 --- a/src/HOL/Finite_Set.thy	Thu Jul 01 16:54:42 2010 +0200
     6.2 +++ b/src/HOL/Finite_Set.thy	Thu Jul 01 16:54:44 2010 +0200
     6.3 @@ -530,7 +530,7 @@
     6.4  instance bool :: finite proof
     6.5  qed (simp add: UNIV_bool)
     6.6  
     6.7 -instance * :: (finite, finite) finite proof
     6.8 +instance prod :: (finite, finite) finite proof
     6.9  qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
    6.10  
    6.11  lemma finite_option_UNIV [simp]:
    6.12 @@ -557,7 +557,7 @@
    6.13    qed
    6.14  qed
    6.15  
    6.16 -instance "+" :: (finite, finite) finite proof
    6.17 +instance sum :: (finite, finite) finite proof
    6.18  qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
    6.19  
    6.20  
     7.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Thu Jul 01 16:54:42 2010 +0200
     7.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Thu Jul 01 16:54:44 2010 +0200
     7.3 @@ -18,9 +18,9 @@
     7.4  
     7.5  instance nat :: heap ..
     7.6  
     7.7 -instance "*" :: (heap, heap) heap ..
     7.8 +instance prod :: (heap, heap) heap ..
     7.9  
    7.10 -instance "+" :: (heap, heap) heap ..
    7.11 +instance sum :: (heap, heap) heap ..
    7.12  
    7.13  instance list :: (heap) heap ..
    7.14  
     8.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu Jul 01 16:54:42 2010 +0200
     8.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu Jul 01 16:54:44 2010 +0200
     8.3 @@ -123,7 +123,7 @@
     8.4  import_theory pair;
     8.5  
     8.6  type_maps
     8.7 -    prod > "Product_Type.*";
     8.8 +    prod > Product_Type.prod;
     8.9  
    8.10  const_maps
    8.11      ","       > Pair
     9.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Jul 01 16:54:42 2010 +0200
     9.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Jul 01 16:54:44 2010 +0200
     9.3 @@ -38,9 +38,9 @@
     9.4    bool > bool
     9.5    fun > fun
     9.6    N_1 >  Product_Type.unit
     9.7 -  prod > "Product_Type.*"
     9.8 +  prod > Product_Type.prod
     9.9    num > Nat.nat
    9.10 -  sum > "Sum_Type.+"
    9.11 +  sum > Sum_Type.sum
    9.12  (*  option > Datatype.option*);
    9.13  
    9.14  const_renames
    10.1 --- a/src/HOL/Import/HOL/pair.imp	Thu Jul 01 16:54:42 2010 +0200
    10.2 +++ b/src/HOL/Import/HOL/pair.imp	Thu Jul 01 16:54:44 2010 +0200
    10.3 @@ -7,7 +7,7 @@
    10.4    "LEX" > "LEX_def"
    10.5  
    10.6  type_maps
    10.7 -  "prod" > "Product_Type.*"
    10.8 +  "prod" > "Product_Type.prod"
    10.9  
   10.10  const_maps
   10.11    "pair_case" > "Product_Type.prod_case"
    11.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Thu Jul 01 16:54:42 2010 +0200
    11.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Thu Jul 01 16:54:44 2010 +0200
    11.3 @@ -6,7 +6,7 @@
    11.4    "sum" > "+"
    11.5    "recspace" > "HOLLight.hollight.recspace"
    11.6    "real" > "HOLLight.hollight.real"
    11.7 -  "prod" > "Product_Type.*"
    11.8 +  "prod" > "Product_Type.prod"
    11.9    "option" > "HOLLight.hollight.option"
   11.10    "num" > "Nat.nat"
   11.11    "nadd" > "HOLLight.hollight.nadd"
    12.1 --- a/src/HOL/Lambda/WeakNorm.thy	Thu Jul 01 16:54:42 2010 +0200
    12.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Thu Jul 01 16:54:44 2010 +0200
    12.3 @@ -349,7 +349,7 @@
    12.4  
    12.5  end
    12.6  
    12.7 -instantiation * :: (default, default) default
    12.8 +instantiation prod :: (default, default) default
    12.9  begin
   12.10  
   12.11  definition "default = (default, default)"
    13.1 --- a/src/HOL/Lattice/Lattice.thy	Thu Jul 01 16:54:42 2010 +0200
    13.2 +++ b/src/HOL/Lattice/Lattice.thy	Thu Jul 01 16:54:44 2010 +0200
    13.3 @@ -453,7 +453,7 @@
    13.4    qed
    13.5  qed
    13.6  
    13.7 -instance * :: (lattice, lattice) lattice
    13.8 +instance prod :: (lattice, lattice) lattice
    13.9  proof
   13.10    fix p q :: "'a::lattice \<times> 'b::lattice"
   13.11    from is_inf_prod show "\<exists>inf. is_inf p q inf" ..
    14.1 --- a/src/HOL/Lattice/Orders.thy	Thu Jul 01 16:54:42 2010 +0200
    14.2 +++ b/src/HOL/Lattice/Orders.thy	Thu Jul 01 16:54:44 2010 +0200
    14.3 @@ -196,7 +196,7 @@
    14.4    \emph{not} be linear in general.
    14.5  *}
    14.6  
    14.7 -instantiation * :: (leq, leq) leq
    14.8 +instantiation prod :: (leq, leq) leq
    14.9  begin
   14.10  
   14.11  definition
   14.12 @@ -214,7 +214,7 @@
   14.13      "p \<sqsubseteq> q \<Longrightarrow> (fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> C) \<Longrightarrow> C"
   14.14    by (unfold leq_prod_def) blast
   14.15  
   14.16 -instance * :: (quasi_order, quasi_order) quasi_order
   14.17 +instance prod :: (quasi_order, quasi_order) quasi_order
   14.18  proof
   14.19    fix p q r :: "'a::quasi_order \<times> 'b::quasi_order"
   14.20    show "p \<sqsubseteq> p"
   14.21 @@ -234,7 +234,7 @@
   14.22    qed
   14.23  qed
   14.24  
   14.25 -instance * :: (partial_order, partial_order) partial_order
   14.26 +instance prod :: (partial_order, partial_order) partial_order
   14.27  proof
   14.28    fix p q :: "'a::partial_order \<times> 'b::partial_order"
   14.29    assume pq: "p \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"
    15.1 --- a/src/HOL/Library/Countable.thy	Thu Jul 01 16:54:42 2010 +0200
    15.2 +++ b/src/HOL/Library/Countable.thy	Thu Jul 01 16:54:44 2010 +0200
    15.3 @@ -63,14 +63,14 @@
    15.4  
    15.5  text {* Pairs *}
    15.6  
    15.7 -instance "*" :: (countable, countable) countable
    15.8 +instance prod :: (countable, countable) countable
    15.9    by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"])
   15.10      (auto simp add: prod_encode_eq)
   15.11  
   15.12  
   15.13  text {* Sums *}
   15.14  
   15.15 -instance "+" :: (countable, countable) countable
   15.16 +instance sum :: (countable, countable) countable
   15.17    by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
   15.18                                       | Inr b \<Rightarrow> to_nat (True, to_nat b))"])
   15.19      (simp split: sum.split_asm)
    16.1 --- a/src/HOL/Library/Enum.thy	Thu Jul 01 16:54:42 2010 +0200
    16.2 +++ b/src/HOL/Library/Enum.thy	Thu Jul 01 16:54:44 2010 +0200
    16.3 @@ -209,7 +209,7 @@
    16.4    using assms by (induct xs)
    16.5      (auto intro: inj_onI simp add: product_list_set distinct_map)
    16.6  
    16.7 -instantiation * :: (enum, enum) enum
    16.8 +instantiation prod :: (enum, enum) enum
    16.9  begin
   16.10  
   16.11  definition
   16.12 @@ -220,7 +220,7 @@
   16.13  
   16.14  end
   16.15  
   16.16 -instantiation "+" :: (enum, enum) enum
   16.17 +instantiation sum :: (enum, enum) enum
   16.18  begin
   16.19  
   16.20  definition
    17.1 --- a/src/HOL/Library/Product_Vector.thy	Thu Jul 01 16:54:42 2010 +0200
    17.2 +++ b/src/HOL/Library/Product_Vector.thy	Thu Jul 01 16:54:44 2010 +0200
    17.3 @@ -10,7 +10,7 @@
    17.4  
    17.5  subsection {* Product is a real vector space *}
    17.6  
    17.7 -instantiation "*" :: (real_vector, real_vector) real_vector
    17.8 +instantiation prod :: (real_vector, real_vector) real_vector
    17.9  begin
   17.10  
   17.11  definition scaleR_prod_def:
   17.12 @@ -41,8 +41,7 @@
   17.13  
   17.14  subsection {* Product is a topological space *}
   17.15  
   17.16 -instantiation
   17.17 -  "*" :: (topological_space, topological_space) topological_space
   17.18 +instantiation prod :: (topological_space, topological_space) topological_space
   17.19  begin
   17.20  
   17.21  definition open_prod_def:
   17.22 @@ -157,8 +156,7 @@
   17.23  
   17.24  subsection {* Product is a metric space *}
   17.25  
   17.26 -instantiation
   17.27 -  "*" :: (metric_space, metric_space) metric_space
   17.28 +instantiation prod :: (metric_space, metric_space) metric_space
   17.29  begin
   17.30  
   17.31  definition dist_prod_def:
   17.32 @@ -340,7 +338,7 @@
   17.33  
   17.34  subsection {* Product is a complete metric space *}
   17.35  
   17.36 -instance "*" :: (complete_space, complete_space) complete_space
   17.37 +instance prod :: (complete_space, complete_space) complete_space
   17.38  proof
   17.39    fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
   17.40    have 1: "(\<lambda>n. fst (X n)) ----> lim (\<lambda>n. fst (X n))"
   17.41 @@ -357,8 +355,7 @@
   17.42  
   17.43  subsection {* Product is a normed vector space *}
   17.44  
   17.45 -instantiation
   17.46 -  "*" :: (real_normed_vector, real_normed_vector) real_normed_vector
   17.47 +instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
   17.48  begin
   17.49  
   17.50  definition norm_prod_def:
   17.51 @@ -397,11 +394,11 @@
   17.52  
   17.53  end
   17.54  
   17.55 -instance "*" :: (banach, banach) banach ..
   17.56 +instance prod :: (banach, banach) banach ..
   17.57  
   17.58  subsection {* Product is an inner product space *}
   17.59  
   17.60 -instantiation "*" :: (real_inner, real_inner) real_inner
   17.61 +instantiation prod :: (real_inner, real_inner) real_inner
   17.62  begin
   17.63  
   17.64  definition inner_prod_def:
    18.1 --- a/src/HOL/Library/Product_ord.thy	Thu Jul 01 16:54:42 2010 +0200
    18.2 +++ b/src/HOL/Library/Product_ord.thy	Thu Jul 01 16:54:44 2010 +0200
    18.3 @@ -8,7 +8,7 @@
    18.4  imports Main
    18.5  begin
    18.6  
    18.7 -instantiation "*" :: (ord, ord) ord
    18.8 +instantiation prod :: (ord, ord) ord
    18.9  begin
   18.10  
   18.11  definition
   18.12 @@ -26,16 +26,16 @@
   18.13    "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
   18.14    unfolding prod_le_def prod_less_def by simp_all
   18.15  
   18.16 -instance * :: (preorder, preorder) preorder proof
   18.17 +instance prod :: (preorder, preorder) preorder proof
   18.18  qed (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
   18.19  
   18.20 -instance * :: (order, order) order proof
   18.21 +instance prod :: (order, order) order proof
   18.22  qed (auto simp add: prod_le_def)
   18.23  
   18.24 -instance * :: (linorder, linorder) linorder proof
   18.25 +instance prod :: (linorder, linorder) linorder proof
   18.26  qed (auto simp: prod_le_def)
   18.27  
   18.28 -instantiation * :: (linorder, linorder) distrib_lattice
   18.29 +instantiation prod :: (linorder, linorder) distrib_lattice
   18.30  begin
   18.31  
   18.32  definition
   18.33 @@ -49,7 +49,7 @@
   18.34  
   18.35  end
   18.36  
   18.37 -instantiation * :: (bot, bot) bot
   18.38 +instantiation prod :: (bot, bot) bot
   18.39  begin
   18.40  
   18.41  definition
   18.42 @@ -60,7 +60,7 @@
   18.43  
   18.44  end
   18.45  
   18.46 -instantiation * :: (top, top) top
   18.47 +instantiation prod :: (top, top) top
   18.48  begin
   18.49  
   18.50  definition
    19.1 --- a/src/HOL/Library/Product_plus.thy	Thu Jul 01 16:54:42 2010 +0200
    19.2 +++ b/src/HOL/Library/Product_plus.thy	Thu Jul 01 16:54:44 2010 +0200
    19.3 @@ -10,7 +10,7 @@
    19.4  
    19.5  subsection {* Operations *}
    19.6  
    19.7 -instantiation "*" :: (zero, zero) zero
    19.8 +instantiation prod :: (zero, zero) zero
    19.9  begin
   19.10  
   19.11  definition zero_prod_def: "0 = (0, 0)"
   19.12 @@ -18,7 +18,7 @@
   19.13  instance ..
   19.14  end
   19.15  
   19.16 -instantiation "*" :: (plus, plus) plus
   19.17 +instantiation prod :: (plus, plus) plus
   19.18  begin
   19.19  
   19.20  definition plus_prod_def:
   19.21 @@ -27,7 +27,7 @@
   19.22  instance ..
   19.23  end
   19.24  
   19.25 -instantiation "*" :: (minus, minus) minus
   19.26 +instantiation prod :: (minus, minus) minus
   19.27  begin
   19.28  
   19.29  definition minus_prod_def:
   19.30 @@ -36,7 +36,7 @@
   19.31  instance ..
   19.32  end
   19.33  
   19.34 -instantiation "*" :: (uminus, uminus) uminus
   19.35 +instantiation prod :: (uminus, uminus) uminus
   19.36  begin
   19.37  
   19.38  definition uminus_prod_def:
   19.39 @@ -83,33 +83,33 @@
   19.40  
   19.41  subsection {* Class instances *}
   19.42  
   19.43 -instance "*" :: (semigroup_add, semigroup_add) semigroup_add
   19.44 +instance prod :: (semigroup_add, semigroup_add) semigroup_add
   19.45    by default (simp add: expand_prod_eq add_assoc)
   19.46  
   19.47 -instance "*" :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
   19.48 +instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
   19.49    by default (simp add: expand_prod_eq add_commute)
   19.50  
   19.51 -instance "*" :: (monoid_add, monoid_add) monoid_add
   19.52 +instance prod :: (monoid_add, monoid_add) monoid_add
   19.53    by default (simp_all add: expand_prod_eq)
   19.54  
   19.55 -instance "*" :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
   19.56 +instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
   19.57    by default (simp add: expand_prod_eq)
   19.58  
   19.59 -instance "*" ::
   19.60 +instance prod ::
   19.61    (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
   19.62      by default (simp_all add: expand_prod_eq)
   19.63  
   19.64 -instance "*" ::
   19.65 +instance prod ::
   19.66    (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
   19.67      by default (simp add: expand_prod_eq)
   19.68  
   19.69 -instance "*" ::
   19.70 +instance prod ::
   19.71    (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
   19.72  
   19.73 -instance "*" :: (group_add, group_add) group_add
   19.74 +instance prod :: (group_add, group_add) group_add
   19.75    by default (simp_all add: expand_prod_eq diff_minus)
   19.76  
   19.77 -instance "*" :: (ab_group_add, ab_group_add) ab_group_add
   19.78 +instance prod :: (ab_group_add, ab_group_add) ab_group_add
   19.79    by default (simp_all add: expand_prod_eq)
   19.80  
   19.81  lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
    20.1 --- a/src/HOL/Library/Quotient_Product.thy	Thu Jul 01 16:54:42 2010 +0200
    20.2 +++ b/src/HOL/Library/Quotient_Product.thy	Thu Jul 01 16:54:44 2010 +0200
    20.3 @@ -13,7 +13,7 @@
    20.4  where
    20.5    "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    20.6  
    20.7 -declare [[map * = (prod_fun, prod_rel)]]
    20.8 +declare [[map prod = (prod_fun, prod_rel)]]
    20.9  
   20.10  
   20.11  lemma prod_equivp[quot_equiv]:
    21.1 --- a/src/HOL/Library/Quotient_Sum.thy	Thu Jul 01 16:54:42 2010 +0200
    21.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Thu Jul 01 16:54:44 2010 +0200
    21.3 @@ -22,7 +22,7 @@
    21.4    "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    21.5  | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    21.6  
    21.7 -declare [[map "+" = (sum_map, sum_rel)]]
    21.8 +declare [[map sum = (sum_map, sum_rel)]]
    21.9  
   21.10  
   21.11  text {* should probably be in @{theory Sum_Type} *}
    22.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jul 01 16:54:42 2010 +0200
    22.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jul 01 16:54:44 2010 +0200
    22.3 @@ -5,7 +5,7 @@
    22.4  imports Finite_Cartesian_Product Integration
    22.5  begin
    22.6  
    22.7 -instantiation * :: (real_basis, real_basis) real_basis
    22.8 +instantiation prod :: (real_basis, real_basis) real_basis
    22.9  begin
   22.10  
   22.11  definition "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))"
   22.12 @@ -131,7 +131,7 @@
   22.13  lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::real_basis) + DIM('a::real_basis)"
   22.14    by (rule dimension_eq) (auto simp: basis_prod_def zero_prod_def basis_eq_0_iff)
   22.15  
   22.16 -instance * :: (euclidean_space, euclidean_space) euclidean_space
   22.17 +instance prod :: (euclidean_space, euclidean_space) euclidean_space
   22.18  proof (default, safe)
   22.19    let ?b = "basis :: nat \<Rightarrow> 'a \<times> 'b"
   22.20    fix i j assume "i < DIM('a \<times> 'b)" "j < DIM('a \<times> 'b)"
   22.21 @@ -139,7 +139,7 @@
   22.22      unfolding basis_prod_def by (auto simp: dot_basis)
   22.23  qed
   22.24  
   22.25 -instantiation * :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
   22.26 +instantiation prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
   22.27  begin
   22.28  
   22.29  definition "x \<le> (y::('a\<times>'b)) \<longleftrightarrow> (\<forall>i<DIM('a\<times>'b). x $$ i \<le> y $$ i)"
    23.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jul 01 16:54:42 2010 +0200
    23.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jul 01 16:54:44 2010 +0200
    23.3 @@ -2422,7 +2422,7 @@
    23.4  apply (erule order_trans [OF real_sqrt_sum_squares_ge2])
    23.5  done
    23.6  
    23.7 -instance "*" :: (heine_borel, heine_borel) heine_borel
    23.8 +instance prod :: (heine_borel, heine_borel) heine_borel
    23.9  proof
   23.10    fix s :: "('a * 'b) set" and f :: "nat \<Rightarrow> 'a * 'b"
   23.11    assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
    24.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Thu Jul 01 16:54:42 2010 +0200
    24.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Jul 01 16:54:44 2010 +0200
    24.3 @@ -543,7 +543,7 @@
    24.4          |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    24.5          |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    24.6          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    24.7 -        |> AxClass.prove_arity (@{type_name "*"},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    24.8 +        |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    24.9          |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   24.10                                      (pt_proof pt_thm_nprod)
   24.11          |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
   24.12 @@ -604,7 +604,7 @@
   24.13          in 
   24.14           thy
   24.15           |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
   24.16 -         |> AxClass.prove_arity (@{type_name "*"},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
   24.17 +         |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
   24.18           |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   24.19                                       (fs_proof fs_thm_nprod) 
   24.20           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
   24.21 @@ -686,7 +686,7 @@
   24.22          in
   24.23           thy'
   24.24           |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
   24.25 -         |> AxClass.prove_arity (@{type_name "*"}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
   24.26 +         |> AxClass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
   24.27           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
   24.28           |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
   24.29           |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
    25.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Thu Jul 01 16:54:42 2010 +0200
    25.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Jul 01 16:54:44 2010 +0200
    25.3 @@ -103,7 +103,7 @@
    25.4      case redex of 
    25.5          (* case pi o (f x) == (pi o f) (pi o x)          *)
    25.6          (Const("Nominal.perm",
    25.7 -          Type("fun",[Type("List.list",[Type(@{type_name "*"},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
    25.8 +          Type("fun",[Type("List.list",[Type(@{type_name Product_Type.prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
    25.9              (if (applicable_app f) then
   25.10                let
   25.11                  val name = Long_Name.base_name n
   25.12 @@ -190,8 +190,8 @@
   25.13  fun perm_compose_simproc' sg ss redex =
   25.14    (case redex of
   25.15       (Const ("Nominal.perm", Type ("fun", [Type ("List.list", 
   25.16 -       [Type (@{type_name "*"}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
   25.17 -         Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [U as Type (uname,_),_])]),_])) $ 
   25.18 +       [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
   25.19 +         Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ 
   25.20            pi2 $ t)) =>
   25.21      let
   25.22        val tname' = Long_Name.base_name tname
    26.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Thu Jul 01 16:54:42 2010 +0200
    26.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Thu Jul 01 16:54:44 2010 +0200
    26.3 @@ -103,7 +103,7 @@
    26.4    let fun get_pi_aux s =
    26.5          (case s of
    26.6            (Const (@{const_name "perm"} ,typrm) $
    26.7 -             (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name "*"}, [Type (tyatm,[]),_])]))) $
    26.8 +             (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name Product_Type.prod}, [Type (tyatm,[]),_])]))) $
    26.9                 (Var (n,ty))) =>
   26.10               let
   26.11                  (* FIXME: this should be an operation the library *)
    27.1 --- a/src/HOL/Product_Type.thy	Thu Jul 01 16:54:42 2010 +0200
    27.2 +++ b/src/HOL/Product_Type.thy	Thu Jul 01 16:54:44 2010 +0200
    27.3 @@ -129,7 +129,7 @@
    27.4  definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
    27.5    "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
    27.6  
    27.7 -typedef (prod) ('a, 'b) "*" (infixr "*" 20)
    27.8 +typedef ('a, 'b) prod (infixr "*" 20)
    27.9    = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
   27.10  proof
   27.11    fix a b show "Pair_Rep a b \<in> ?prod"
   27.12 @@ -137,14 +137,14 @@
   27.13  qed
   27.14  
   27.15  type_notation (xsymbols)
   27.16 -  "*"  ("(_ \<times>/ _)" [21, 20] 20)
   27.17 +  "prod"  ("(_ \<times>/ _)" [21, 20] 20)
   27.18  type_notation (HTML output)
   27.19 -  "*"  ("(_ \<times>/ _)" [21, 20] 20)
   27.20 +  "prod"  ("(_ \<times>/ _)" [21, 20] 20)
   27.21  
   27.22  definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
   27.23    "Pair a b = Abs_prod (Pair_Rep a b)"
   27.24  
   27.25 -rep_datatype (prod) Pair proof -
   27.26 +rep_datatype Pair proof -
   27.27    fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
   27.28    assume "\<And>a b. P (Pair a b)"
   27.29    then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
   27.30 @@ -263,7 +263,7 @@
   27.31  
   27.32  subsubsection {* Code generator setup *}
   27.33  
   27.34 -code_type *
   27.35 +code_type prod
   27.36    (SML infix 2 "*")
   27.37    (OCaml infix 2 "*")
   27.38    (Haskell "!((_),/ (_))")
   27.39 @@ -275,19 +275,19 @@
   27.40    (Haskell "!((_),/ (_))")
   27.41    (Scala "!((_),/ (_))")
   27.42  
   27.43 -code_instance * :: eq
   27.44 +code_instance prod :: eq
   27.45    (Haskell -)
   27.46  
   27.47  code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   27.48    (Haskell infixl 4 "==")
   27.49  
   27.50  types_code
   27.51 -  "*"     ("(_ */ _)")
   27.52 +  "prod"     ("(_ */ _)")
   27.53  attach (term_of) {*
   27.54 -fun term_of_id_42 aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
   27.55 +fun term_of_prod aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
   27.56  *}
   27.57  attach (test) {*
   27.58 -fun gen_id_42 aG aT bG bT i =
   27.59 +fun term_of_prod aG aT bG bT i =
   27.60    let
   27.61      val (x, t) = aG i;
   27.62      val (y, u) = bG i
   27.63 @@ -438,7 +438,7 @@
   27.64  
   27.65  lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
   27.66    -- {* Prevents simplification of @{term c}: much faster *}
   27.67 -  by (erule arg_cong)
   27.68 +  by (fact weak_case_cong)
   27.69  
   27.70  lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
   27.71    by (simp add: split_eta)
   27.72 @@ -689,19 +689,18 @@
   27.73  lemmas prod_caseI = prod.cases [THEN iffD2, standard]
   27.74  
   27.75  lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
   27.76 -  by auto
   27.77 +  by (fact splitI2)
   27.78  
   27.79  lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x"
   27.80 -  by (auto simp: split_tupled_all)
   27.81 +  by (fact splitI2')
   27.82  
   27.83  lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   27.84 -  by (induct p) auto
   27.85 +  by (fact splitE)
   27.86  
   27.87  lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   27.88 -  by (induct p) auto
   27.89 +  by (fact splitE')
   27.90  
   27.91 -declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
   27.92 -declare prod_caseE' [elim!] prod_caseE [elim!]
   27.93 +declare prod_caseI [intro!]
   27.94  
   27.95  lemma prod_case_beta:
   27.96    "prod_case f p = f (fst p) (snd p)"
   27.97 @@ -795,8 +794,11 @@
   27.98  definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60) where
   27.99    "f o\<rightarrow> g = (\<lambda>x. split g (f x))"
  27.100  
  27.101 +lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
  27.102 +  by (simp add: expand_fun_eq scomp_def split_def)
  27.103 +
  27.104  lemma scomp_apply:  "(f o\<rightarrow> g) x = split g (f x)"
  27.105 -  by (simp add: scomp_def)
  27.106 +  by (simp add: scomp_unfold split_def)
  27.107  
  27.108  lemma Pair_scomp: "Pair x o\<rightarrow> f = f x"
  27.109    by (simp add: expand_fun_eq scomp_apply)
  27.110 @@ -805,13 +807,13 @@
  27.111    by (simp add: expand_fun_eq scomp_apply)
  27.112  
  27.113  lemma scomp_scomp: "(f o\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)"
  27.114 -  by (simp add: expand_fun_eq split_twice scomp_def)
  27.115 +  by (simp add: expand_fun_eq scomp_unfold)
  27.116  
  27.117  lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>x. g x o> h)"
  27.118 -  by (simp add: expand_fun_eq scomp_apply fcomp_def split_def)
  27.119 +  by (simp add: expand_fun_eq scomp_unfold fcomp_def)
  27.120  
  27.121  lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)"
  27.122 -  by (simp add: expand_fun_eq scomp_apply fcomp_apply)
  27.123 +  by (simp add: expand_fun_eq scomp_unfold fcomp_apply)
  27.124  
  27.125  code_const scomp
  27.126    (Eval infixl 3 "#->")
    28.1 --- a/src/HOL/Sum_Type.thy	Thu Jul 01 16:54:42 2010 +0200
    28.2 +++ b/src/HOL/Sum_Type.thy	Thu Jul 01 16:54:44 2010 +0200
    28.3 @@ -17,7 +17,7 @@
    28.4  definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
    28.5    "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
    28.6  
    28.7 -typedef (sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
    28.8 +typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
    28.9    by auto
   28.10  
   28.11  lemma Inl_RepI: "Inl_Rep a \<in> sum"
   28.12 @@ -83,7 +83,7 @@
   28.13    with assms show P by (auto simp add: sum_def Inl_def Inr_def)
   28.14  qed
   28.15  
   28.16 -rep_datatype (sum) Inl Inr
   28.17 +rep_datatype Inl Inr
   28.18  proof -
   28.19    fix P
   28.20    fix s :: "'a + 'b"
    29.1 --- a/src/HOL/TLA/Action.thy	Thu Jul 01 16:54:42 2010 +0200
    29.2 +++ b/src/HOL/TLA/Action.thy	Thu Jul 01 16:54:44 2010 +0200
    29.3 @@ -16,8 +16,7 @@
    29.4    'a trfun = "(state * state) => 'a"
    29.5    action   = "bool trfun"
    29.6  
    29.7 -arities
    29.8 -  "*" :: (world, world) world
    29.9 +arities prod :: (world, world) world
   29.10  
   29.11  consts
   29.12    (** abstract syntax **)
    30.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Thu Jul 01 16:54:42 2010 +0200
    30.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Jul 01 16:54:44 2010 +0200
    30.3 @@ -75,7 +75,7 @@
    30.4      val leafTs' = get_nonrec_types descr' sorts;
    30.5      val branchTs = get_branching_types descr' sorts;
    30.6      val branchT = if null branchTs then HOLogic.unitT
    30.7 -      else Balanced_Tree.make (fn (T, U) => Type (@{type_name "+"}, [T, U])) branchTs;
    30.8 +      else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
    30.9      val arities = remove (op =) 0 (get_arities descr');
   30.10      val unneeded_vars =
   30.11        subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
   30.12 @@ -83,7 +83,7 @@
   30.13      val recTs = get_rec_types descr' sorts;
   30.14      val (newTs, oldTs) = chop (length (hd descr)) recTs;
   30.15      val sumT = if null leafTs then HOLogic.unitT
   30.16 -      else Balanced_Tree.make (fn (T, U) => Type (@{type_name "+"}, [T, U])) leafTs;
   30.17 +      else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) leafTs;
   30.18      val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
   30.19      val UnivT = HOLogic.mk_setT Univ_elT;
   30.20      val UnivT' = Univ_elT --> HOLogic.boolT;
    31.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Thu Jul 01 16:54:42 2010 +0200
    31.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Thu Jul 01 16:54:44 2010 +0200
    31.3 @@ -39,17 +39,17 @@
    31.4  fun constant_0 T = Abs ("x", T, HOLogic.zero)
    31.5  fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
    31.6  
    31.7 -fun mk_funorder_funs (Type (@{type_name "+"}, [fT, sT])) =
    31.8 +fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
    31.9    map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
   31.10    @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
   31.11    | mk_funorder_funs T = [ constant_1 T ]
   31.12  
   31.13 -fun mk_ext_base_funs ctxt (Type (@{type_name "+"}, [fT, sT])) =
   31.14 +fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
   31.15      map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
   31.16        (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
   31.17    | mk_ext_base_funs ctxt T = find_measures ctxt T
   31.18  
   31.19 -fun mk_all_measure_funs ctxt (T as Type (@{type_name "+"}, _)) =
   31.20 +fun mk_all_measure_funs ctxt (T as Type (@{type_name Sum_Type.sum}, _)) =
   31.21      mk_ext_base_funs ctxt T @ mk_funorder_funs T
   31.22    | mk_all_measure_funs ctxt T = find_measures ctxt T
   31.23  
    32.1 --- a/src/HOL/Tools/Function/sum_tree.ML	Thu Jul 01 16:54:42 2010 +0200
    32.2 +++ b/src/HOL/Tools/Function/sum_tree.ML	Thu Jul 01 16:54:44 2010 +0200
    32.3 @@ -17,7 +17,7 @@
    32.4      {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
    32.5  
    32.6  (* Sum types *)
    32.7 -fun mk_sumT LT RT = Type (@{type_name "+"}, [LT, RT])
    32.8 +fun mk_sumT LT RT = Type (@{type_name Sum_Type.sum}, [LT, RT])
    32.9  fun mk_sumcase TL TR T l r =
   32.10    Const (@{const_name sum.sum_case},
   32.11      (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
   32.12 @@ -27,18 +27,18 @@
   32.13  fun mk_inj ST n i =
   32.14    access_top_down
   32.15    { init = (ST, I : term -> term),
   32.16 -    left = (fn (T as Type (@{type_name "+"}, [LT, RT]), inj) =>
   32.17 +    left = (fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), inj) =>
   32.18        (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
   32.19 -    right =(fn (T as Type (@{type_name "+"}, [LT, RT]), inj) =>
   32.20 +    right =(fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), inj) =>
   32.21        (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i
   32.22    |> snd
   32.23  
   32.24  fun mk_proj ST n i =
   32.25    access_top_down
   32.26    { init = (ST, I : term -> term),
   32.27 -    left = (fn (T as Type (@{type_name "+"}, [LT, RT]), proj) =>
   32.28 +    left = (fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) =>
   32.29        (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
   32.30 -    right =(fn (T as Type (@{type_name "+"}, [LT, RT]), proj) =>
   32.31 +    right =(fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) =>
   32.32        (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
   32.33    |> snd
   32.34  
    33.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Jul 01 16:54:42 2010 +0200
    33.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Jul 01 16:54:44 2010 +0200
    33.3 @@ -106,7 +106,7 @@
    33.4    end
    33.5  
    33.6  (* compute list of types for nodes *)
    33.7 -fun node_types sk T = dest_tree (fn Type (@{type_name "+"}, [LT, RT]) => (LT, RT)) sk T |> map snd
    33.8 +fun node_types sk T = dest_tree (fn Type (@{type_name Sum_Type.sum}, [LT, RT]) => (LT, RT)) sk T |> map snd
    33.9  
   33.10  (* find index and raw term *)
   33.11  fun dest_inj (SLeaf i) trm = (i, trm)
    34.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Thu Jul 01 16:54:42 2010 +0200
    34.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Thu Jul 01 16:54:44 2010 +0200
    34.3 @@ -37,7 +37,7 @@
    34.4  
    34.5  fun check_type ctxt (Type (@{type_name fun}, Ts)) =
    34.6      List.app (check_type ctxt) Ts
    34.7 -  | check_type ctxt (Type (@{type_name "*"}, Ts)) =
    34.8 +  | check_type ctxt (Type (@{type_name Product_Type.prod}, Ts)) =
    34.9      List.app (check_type ctxt) Ts
   34.10    | check_type _ @{typ bool} = ()
   34.11    | check_type _ (TFree (_, @{sort "{}"})) = ()
   34.12 @@ -51,7 +51,7 @@
   34.13      atom_schema_of SRep card T1
   34.14    | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
   34.15      atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
   34.16 -  | atom_schema_of _ card (Type (@{type_name "*"}, Ts)) =
   34.17 +  | atom_schema_of _ card (Type (@{type_name Product_Type.prod}, Ts)) =
   34.18      maps (atom_schema_of SRep card) Ts
   34.19    | atom_schema_of _ card T = [card T]
   34.20  val arity_of = length ooo atom_schema_of
   34.21 @@ -290,7 +290,7 @@
   34.22      val thy = ProofContext.theory_of ctxt
   34.23      fun card (Type (@{type_name fun}, [T1, T2])) =
   34.24          reasonable_power (card T2) (card T1)
   34.25 -      | card (Type (@{type_name "*"}, [T1, T2])) = card T1 * card T2
   34.26 +      | card (Type (@{type_name Product_Type.prod}, [T1, T2])) = card T1 * card T2
   34.27        | card @{typ bool} = 2
   34.28        | card T = Int.max (1, raw_card T)
   34.29      val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
    35.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Jul 01 16:54:42 2010 +0200
    35.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Jul 01 16:54:44 2010 +0200
    35.3 @@ -454,7 +454,7 @@
    35.4    | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
    35.5      unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
    35.6    | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
    35.7 -    Type (@{type_name "*"}, map unarize_unbox_etc_type Ts)
    35.8 +    Type (@{type_name Product_Type.prod}, map unarize_unbox_etc_type Ts)
    35.9    | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T
   35.10    | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T
   35.11    | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
   35.12 @@ -509,7 +509,7 @@
   35.13    | is_fun_type _ = false
   35.14  fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
   35.15    | is_set_type _ = false
   35.16 -fun is_pair_type (Type (@{type_name "*"}, _)) = true
   35.17 +fun is_pair_type (Type (@{type_name Product_Type.prod}, _)) = true
   35.18    | is_pair_type _ = false
   35.19  fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
   35.20    | is_lfp_iterator_type _ = false
   35.21 @@ -546,7 +546,7 @@
   35.22    | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
   35.23  val nth_range_type = snd oo strip_n_binders
   35.24  
   35.25 -fun num_factors_in_type (Type (@{type_name "*"}, [T1, T2])) =
   35.26 +fun num_factors_in_type (Type (@{type_name Product_Type.prod}, [T1, T2])) =
   35.27      fold (Integer.add o num_factors_in_type) [T1, T2] 0
   35.28    | num_factors_in_type _ = 1
   35.29  fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
   35.30 @@ -557,7 +557,7 @@
   35.31    (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
   35.32  
   35.33  fun mk_flat_tuple _ [t] = t
   35.34 -  | mk_flat_tuple (Type (@{type_name "*"}, [T1, T2])) (t :: ts) =
   35.35 +  | mk_flat_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) (t :: ts) =
   35.36      HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
   35.37    | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
   35.38  fun dest_n_tuple 1 t = [t]
   35.39 @@ -595,7 +595,7 @@
   35.40  (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
   35.41     e.g., by adding a field to "Datatype_Aux.info". *)
   35.42  fun is_basic_datatype thy stds s =
   35.43 -  member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
   35.44 +  member (op =) [@{type_name Product_Type.prod}, @{type_name bool}, @{type_name unit},
   35.45                   @{type_name int}, "Code_Numeral.code_numeral"] s orelse
   35.46    (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
   35.47  
   35.48 @@ -792,7 +792,7 @@
   35.49      Type (@{type_name fun}, _) =>
   35.50      (boxy = InPair orelse boxy = InFunLHS) andalso
   35.51      not (is_boolean_type (body_type T))
   35.52 -  | Type (@{type_name "*"}, Ts) =>
   35.53 +  | Type (@{type_name Product_Type.prod}, Ts) =>
   35.54      boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
   35.55      ((boxy = InExpr orelse boxy = InFunLHS) andalso
   35.56       exists (is_boxing_worth_it hol_ctxt InPair)
   35.57 @@ -812,12 +812,12 @@
   35.58      else
   35.59        box_type hol_ctxt (in_fun_lhs_for boxy) T1
   35.60        --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
   35.61 -  | Type (z as (@{type_name "*"}, Ts)) =>
   35.62 +  | Type (z as (@{type_name Product_Type.prod}, Ts)) =>
   35.63      if boxy <> InConstr andalso boxy <> InSel
   35.64         andalso should_box_type hol_ctxt boxy z then
   35.65        Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
   35.66      else
   35.67 -      Type (@{type_name "*"},
   35.68 +      Type (@{type_name Product_Type.prod},
   35.69              map (box_type hol_ctxt
   35.70                            (if boxy = InConstr orelse boxy = InSel then boxy
   35.71                             else InPair)) Ts)
   35.72 @@ -979,7 +979,7 @@
   35.73        Const (nth_sel_for_constr x n)
   35.74      else
   35.75        let
   35.76 -        fun aux m (Type (@{type_name "*"}, [T1, T2])) =
   35.77 +        fun aux m (Type (@{type_name Product_Type.prod}, [T1, T2])) =
   35.78              let
   35.79                val (m, t1) = aux m T1
   35.80                val (m, t2) = aux m T2
   35.81 @@ -1069,7 +1069,7 @@
   35.82      | (Type (new_s, new_Ts as [new_T1, new_T2]),
   35.83         Type (old_s, old_Ts as [old_T1, old_T2])) =>
   35.84        if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
   35.85 -         old_s = @{type_name pair_box} orelse old_s = @{type_name "*"} then
   35.86 +         old_s = @{type_name pair_box} orelse old_s = @{type_name Product_Type.prod} then
   35.87          case constr_expand hol_ctxt old_T t of
   35.88            Const (old_s, _) $ t1 =>
   35.89            if new_s = @{type_name fun} then
   35.90 @@ -1081,7 +1081,7 @@
   35.91                               (Type (@{type_name fun}, old_Ts)) t1]
   35.92          | Const _ $ t1 $ t2 =>
   35.93            construct_value ctxt stds
   35.94 -              (if new_s = @{type_name "*"} then @{const_name Pair}
   35.95 +              (if new_s = @{type_name Product_Type.prod} then @{const_name Pair}
   35.96                 else @{const_name PairBox}, new_Ts ---> new_T)
   35.97                (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
   35.98                      [t1, t2])
   35.99 @@ -1092,7 +1092,7 @@
  35.100  
  35.101  fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
  35.102      reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
  35.103 -  | card_of_type assigns (Type (@{type_name "*"}, [T1, T2])) =
  35.104 +  | card_of_type assigns (Type (@{type_name Product_Type.prod}, [T1, T2])) =
  35.105      card_of_type assigns T1 * card_of_type assigns T2
  35.106    | card_of_type _ (Type (@{type_name itself}, _)) = 1
  35.107    | card_of_type _ @{typ prop} = 2
  35.108 @@ -1113,7 +1113,7 @@
  35.109        else Int.min (max, reasonable_power k2 k1)
  35.110      end
  35.111    | bounded_card_of_type max default_card assigns
  35.112 -                         (Type (@{type_name "*"}, [T1, T2])) =
  35.113 +                         (Type (@{type_name Product_Type.prod}, [T1, T2])) =
  35.114      let
  35.115        val k1 = bounded_card_of_type max default_card assigns T1
  35.116        val k2 = bounded_card_of_type max default_card assigns T2
  35.117 @@ -1143,7 +1143,7 @@
  35.118             else if k1 >= max orelse k2 >= max then max
  35.119             else Int.min (max, reasonable_power k2 k1)
  35.120           end
  35.121 -       | Type (@{type_name "*"}, [T1, T2]) =>
  35.122 +       | Type (@{type_name Product_Type.prod}, [T1, T2]) =>
  35.123           let
  35.124             val k1 = aux avoid T1
  35.125             val k2 = aux avoid T2
  35.126 @@ -1196,7 +1196,7 @@
  35.127    fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
  35.128  
  35.129  fun is_funky_typedef_name thy s =
  35.130 -  member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
  35.131 +  member (op =) [@{type_name unit}, @{type_name Product_Type.prod}, @{type_name Sum_Type.sum},
  35.132                   @{type_name int}] s orelse
  35.133    is_frac_type thy (Type (s, []))
  35.134  fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
  35.135 @@ -2066,7 +2066,7 @@
  35.136      val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
  35.137      val set_T = tuple_T --> bool_T
  35.138      val curried_T = tuple_T --> set_T
  35.139 -    val uncurried_T = Type (@{type_name "*"}, [tuple_T, tuple_T]) --> bool_T
  35.140 +    val uncurried_T = Type (@{type_name Product_Type.prod}, [tuple_T, tuple_T]) --> bool_T
  35.141      val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
  35.142      val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
  35.143      val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
  35.144 @@ -2185,7 +2185,7 @@
  35.145      fun aux T accum =
  35.146        case T of
  35.147          Type (@{type_name fun}, Ts) => fold aux Ts accum
  35.148 -      | Type (@{type_name "*"}, Ts) => fold aux Ts accum
  35.149 +      | Type (@{type_name Product_Type.prod}, Ts) => fold aux Ts accum
  35.150        | Type (@{type_name itself}, [T1]) => aux T1 accum
  35.151        | Type (_, Ts) =>
  35.152          if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
    36.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Jul 01 16:54:42 2010 +0200
    36.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Jul 01 16:54:44 2010 +0200
    36.3 @@ -170,7 +170,7 @@
    36.4                  Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])]))
    36.5           $ t1 $ t2) =
    36.6      let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in
    36.7 -      Const (@{const_name Pair}, Ts ---> Type (@{type_name "*"}, Ts))
    36.8 +      Const (@{const_name Pair}, Ts ---> Type (@{type_name Product_Type.prod}, Ts))
    36.9        $ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
   36.10      end
   36.11    | unarize_unbox_etc_term (Const (s, T)) =
   36.12 @@ -185,27 +185,27 @@
   36.13    | unarize_unbox_etc_term (Abs (s, T, t')) =
   36.14      Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t')
   36.15  
   36.16 -fun factor_out_types (T1 as Type (@{type_name "*"}, [T11, T12]))
   36.17 -                     (T2 as Type (@{type_name "*"}, [T21, T22])) =
   36.18 +fun factor_out_types (T1 as Type (@{type_name Product_Type.prod}, [T11, T12]))
   36.19 +                     (T2 as Type (@{type_name Product_Type.prod}, [T21, T22])) =
   36.20      let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
   36.21        if n1 = n2 then
   36.22          let
   36.23            val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
   36.24          in
   36.25 -          ((Type (@{type_name "*"}, [T11, T11']), opt_T12'),
   36.26 -           (Type (@{type_name "*"}, [T21, T21']), opt_T22'))
   36.27 +          ((Type (@{type_name Product_Type.prod}, [T11, T11']), opt_T12'),
   36.28 +           (Type (@{type_name Product_Type.prod}, [T21, T21']), opt_T22'))
   36.29          end
   36.30        else if n1 < n2 then
   36.31          case factor_out_types T1 T21 of
   36.32            (p1, (T21', NONE)) => (p1, (T21', SOME T22))
   36.33          | (p1, (T21', SOME T22')) =>
   36.34 -          (p1, (T21', SOME (Type (@{type_name "*"}, [T22', T22]))))
   36.35 +          (p1, (T21', SOME (Type (@{type_name Product_Type.prod}, [T22', T22]))))
   36.36        else
   36.37          swap (factor_out_types T2 T1)
   36.38      end
   36.39 -  | factor_out_types (Type (@{type_name "*"}, [T11, T12])) T2 =
   36.40 +  | factor_out_types (Type (@{type_name Product_Type.prod}, [T11, T12])) T2 =
   36.41      ((T11, SOME T12), (T2, NONE))
   36.42 -  | factor_out_types T1 (Type (@{type_name "*"}, [T21, T22])) =
   36.43 +  | factor_out_types T1 (Type (@{type_name Product_Type.prod}, [T21, T22])) =
   36.44      ((T1, NONE), (T21, SOME T22))
   36.45    | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
   36.46  
   36.47 @@ -239,7 +239,7 @@
   36.48      val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
   36.49      val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
   36.50    in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
   36.51 -fun pair_up (Type (@{type_name "*"}, [T1', T2']))
   36.52 +fun pair_up (Type (@{type_name Product_Type.prod}, [T1', T2']))
   36.53              (t1 as Const (@{const_name Pair},
   36.54                            Type (@{type_name fun},
   36.55                                  [_, Type (@{type_name fun}, [_, T1])]))
   36.56 @@ -287,8 +287,8 @@
   36.57        and do_term (Type (@{type_name fun}, [T1', T2']))
   36.58                    (Type (@{type_name fun}, [T1, T2])) t =
   36.59            do_fun T1' T2' T1 T2 t
   36.60 -        | do_term (T' as Type (@{type_name "*"}, Ts' as [T1', T2']))
   36.61 -                  (Type (@{type_name "*"}, [T1, T2]))
   36.62 +        | do_term (T' as Type (@{type_name Product_Type.prod}, Ts' as [T1', T2']))
   36.63 +                  (Type (@{type_name Product_Type.prod}, [T1, T2]))
   36.64                    (Const (@{const_name Pair}, _) $ t1 $ t2) =
   36.65            Const (@{const_name Pair}, Ts' ---> T')
   36.66            $ do_term T1' T1 t1 $ do_term T2' T2 t2
   36.67 @@ -303,7 +303,7 @@
   36.68    | truth_const_sort_key @{const False} = "2"
   36.69    | truth_const_sort_key _ = "1"
   36.70  
   36.71 -fun mk_tuple (Type (@{type_name "*"}, [T1, T2])) ts =
   36.72 +fun mk_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) ts =
   36.73      HOLogic.mk_prod (mk_tuple T1 ts,
   36.74          mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
   36.75    | mk_tuple _ (t :: _) = t
   36.76 @@ -463,7 +463,7 @@
   36.77                              signed_string_of_int j ^ " for " ^
   36.78                              string_for_rep (Vect (k1, Atom (k2, 0))))
   36.79          end
   36.80 -      | term_for_atom seen (Type (@{type_name "*"}, [T1, T2])) _ j k =
   36.81 +      | term_for_atom seen (Type (@{type_name Product_Type.prod}, [T1, T2])) _ j k =
   36.82          let
   36.83            val k1 = card_of_type card_assigns T1
   36.84            val k2 = k div k1
   36.85 @@ -592,7 +592,7 @@
   36.86        | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
   36.87          if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
   36.88          else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
   36.89 -      | term_for_rep _ seen (Type (@{type_name "*"}, [T1, T2])) _
   36.90 +      | term_for_rep _ seen (Type (@{type_name Product_Type.prod}, [T1, T2])) _
   36.91                       (Struct [R1, R2]) [js] =
   36.92          let
   36.93            val arity1 = arity_of_rep R1
    37.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Jul 01 16:54:42 2010 +0200
    37.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Jul 01 16:54:44 2010 +0200
    37.3 @@ -254,7 +254,7 @@
    37.4        else case T of
    37.5          Type (@{type_name fun}, [T1, T2]) =>
    37.6          MFun (fresh_mfun_for_fun_type mdata false T1 T2)
    37.7 -      | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
    37.8 +      | Type (@{type_name Product_Type.prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
    37.9        | Type (z as (s, _)) =>
   37.10          if could_exist_alpha_sub_mtype ctxt alpha_T T then
   37.11            case AList.lookup (op =) (!datatype_mcache) z of
   37.12 @@ -1035,8 +1035,8 @@
   37.13            | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
   37.14              Type (if should_finitize T a then @{type_name fin_fun}
   37.15                    else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
   37.16 -          | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) =>
   37.17 -            Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2])
   37.18 +          | (MPair (M1, M2), Type (@{type_name Product_Type.prod}, Ts)) =>
   37.19 +            Type (@{type_name Product_Type.prod}, map2 type_from_mtype Ts [M1, M2])
   37.20            | (MType _, _) => T
   37.21            | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
   37.22                                [M], [T])
    38.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Jul 01 16:54:42 2010 +0200
    38.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Jul 01 16:54:44 2010 +0200
    38.3 @@ -427,7 +427,7 @@
    38.4      let val res_T = snd (HOLogic.dest_prodT T) in
    38.5        (res_T, Const (@{const_name snd}, T --> res_T) $ t)
    38.6      end
    38.7 -fun factorize (z as (Type (@{type_name "*"}, _), _)) =
    38.8 +fun factorize (z as (Type (@{type_name Product_Type.prod}, _), _)) =
    38.9      maps factorize [mk_fst z, mk_snd z]
   38.10    | factorize z = [z]
   38.11  
   38.12 @@ -1199,7 +1199,7 @@
   38.13      val w = constr (j, type_of v, rep_of v)
   38.14    in (w :: ws, pool, NameTable.update (v, w) table) end
   38.15  
   38.16 -fun shape_tuple (T as Type (@{type_name "*"}, [T1, T2])) (R as Struct [R1, R2])
   38.17 +fun shape_tuple (T as Type (@{type_name Product_Type.prod}, [T1, T2])) (R as Struct [R1, R2])
   38.18                  us =
   38.19      let val arity1 = arity_of_rep R1 in
   38.20        Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
    39.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Jul 01 16:54:42 2010 +0200
    39.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Jul 01 16:54:44 2010 +0200
    39.3 @@ -132,8 +132,8 @@
    39.4    let
    39.5      fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
    39.6          Type (@{type_name fun}, map box_relational_operator_type Ts)
    39.7 -      | box_relational_operator_type (Type (@{type_name "*"}, Ts)) =
    39.8 -        Type (@{type_name "*"}, map (box_type hol_ctxt InPair) Ts)
    39.9 +      | box_relational_operator_type (Type (@{type_name Product_Type.prod}, Ts)) =
   39.10 +        Type (@{type_name Product_Type.prod}, map (box_type hol_ctxt InPair) Ts)
   39.11        | box_relational_operator_type T = T
   39.12      fun add_boxed_types_for_var (z as (_, T)) (T', t') =
   39.13        case t' of
   39.14 @@ -953,7 +953,7 @@
   39.15      and add_axioms_for_type depth T =
   39.16        case T of
   39.17          Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
   39.18 -      | Type (@{type_name "*"}, Ts) => fold (add_axioms_for_type depth) Ts
   39.19 +      | Type (@{type_name Product_Type.prod}, Ts) => fold (add_axioms_for_type depth) Ts
   39.20        | @{typ prop} => I
   39.21        | @{typ bool} => I
   39.22        | @{typ unit} => I
    40.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Thu Jul 01 16:54:42 2010 +0200
    40.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Thu Jul 01 16:54:44 2010 +0200
    40.3 @@ -249,7 +249,7 @@
    40.4      (case best_one_rep_for_type scope T2 of
    40.5         Unit => Unit
    40.6       | R2 => Vect (card_of_type card_assigns T1, R2))
    40.7 -  | best_one_rep_for_type scope (Type (@{type_name "*"}, [T1, T2])) =
    40.8 +  | best_one_rep_for_type scope (Type (@{type_name Product_Type.prod}, [T1, T2])) =
    40.9      (case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
   40.10         (Unit, Unit) => Unit
   40.11       | (R1, R2) => Struct [R1, R2])
   40.12 @@ -302,7 +302,7 @@
   40.13  fun type_schema_of_rep _ (Formula _) = []
   40.14    | type_schema_of_rep _ Unit = []
   40.15    | type_schema_of_rep T (Atom _) = [T]
   40.16 -  | type_schema_of_rep (Type (@{type_name "*"}, [T1, T2])) (Struct [R1, R2]) =
   40.17 +  | type_schema_of_rep (Type (@{type_name Product_Type.prod}, [T1, T2])) (Struct [R1, R2]) =
   40.18      type_schema_of_reps [T1, T2] [R1, R2]
   40.19    | type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) =
   40.20      replicate_list k (type_schema_of_rep T2 R)
    41.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Jul 01 16:54:42 2010 +0200
    41.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Jul 01 16:54:44 2010 +0200
    41.3 @@ -107,7 +107,7 @@
    41.4      is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
    41.5    | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
    41.6      is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
    41.7 -  | is_complete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
    41.8 +  | is_complete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) =
    41.9      forall (is_complete_type dtypes facto) Ts
   41.10    | is_complete_type dtypes facto T =
   41.11      not (is_integer_like_type T) andalso not (is_bit_type T) andalso
   41.12 @@ -117,7 +117,7 @@
   41.13      is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
   41.14    | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
   41.15      is_concrete_type dtypes facto T2
   41.16 -  | is_concrete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
   41.17 +  | is_concrete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) =
   41.18      forall (is_concrete_type dtypes facto) Ts
   41.19    | is_concrete_type dtypes facto T =
   41.20      fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
    42.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jul 01 16:54:42 2010 +0200
    42.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jul 01 16:54:44 2010 +0200
    42.3 @@ -210,7 +210,7 @@
    42.4      else
    42.5        [Input, Output]
    42.6    end
    42.7 -  | all_modes_of_typ' (Type (@{type_name "*"}, [T1, T2])) = 
    42.8 +  | all_modes_of_typ' (Type (@{type_name Product_Type.prod}, [T1, T2])) = 
    42.9      map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2)
   42.10    | all_modes_of_typ' _ = [Input, Output]
   42.11  
   42.12 @@ -230,7 +230,7 @@
   42.13  fun all_smodes_of_typ (T as Type ("fun", _)) =
   42.14    let
   42.15      val (S, U) = strip_type T
   42.16 -    fun all_smodes (Type (@{type_name "*"}, [T1, T2])) = 
   42.17 +    fun all_smodes (Type (@{type_name Product_Type.prod}, [T1, T2])) = 
   42.18        map_product (curry Pair) (all_smodes T1) (all_smodes T2)
   42.19        | all_smodes _ = [Input, Output]
   42.20    in
   42.21 @@ -280,7 +280,7 @@
   42.22  fun ho_argsT_of mode Ts =
   42.23    let
   42.24      fun ho_arg (Fun _) T = [T]
   42.25 -      | ho_arg (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2
   42.26 +      | ho_arg (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2
   42.27        | ho_arg _ _ = []
   42.28    in
   42.29      flat (map2 ho_arg (strip_fun_mode mode) Ts)
   42.30 @@ -309,7 +309,7 @@
   42.31  fun split_map_modeT f mode Ts =
   42.32    let
   42.33      fun split_arg_mode' (m as Fun _) T = f m T
   42.34 -      | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) =
   42.35 +      | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
   42.36          let
   42.37            val (i1, o1) = split_arg_mode' m1 T1
   42.38            val (i2, o2) = split_arg_mode' m2 T2
   42.39 @@ -325,7 +325,7 @@
   42.40  
   42.41  fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts
   42.42  
   42.43 -fun fold_map_aterms_prodT comb f (Type (@{type_name "*"}, [T1, T2])) s =
   42.44 +fun fold_map_aterms_prodT comb f (Type (@{type_name Product_Type.prod}, [T1, T2])) s =
   42.45    let
   42.46      val (x1, s') = fold_map_aterms_prodT comb f T1 s
   42.47      val (x2, s'') = fold_map_aterms_prodT comb f T2 s'
   42.48 @@ -343,7 +343,7 @@
   42.49  fun split_modeT' mode Ts =
   42.50    let
   42.51      fun split_arg_mode' (Fun _) T = ([], [])
   42.52 -      | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) =
   42.53 +      | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
   42.54          let
   42.55            val (i1, o1) = split_arg_mode' m1 T1
   42.56            val (i2, o2) = split_arg_mode' m2 T2
   42.57 @@ -756,9 +756,9 @@
   42.58        (case HOLogic.strip_tupleT (fastype_of arg) of
   42.59          (Ts as _ :: _ :: _) =>
   42.60          let
   42.61 -          fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name "*"}, [_, T2]))
   42.62 +          fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
   42.63              (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
   42.64 -            | rewrite_arg' (t, Type (@{type_name "*"}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
   42.65 +            | rewrite_arg' (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
   42.66                let
   42.67                  val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
   42.68                  val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
    43.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Jul 01 16:54:42 2010 +0200
    43.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Jul 01 16:54:44 2010 +0200
    43.3 @@ -70,7 +70,7 @@
    43.4  fun mk_randompredT T =
    43.5    @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
    43.6  
    43.7 -fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"},
    43.8 +fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
    43.9    [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
   43.10    | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
   43.11  
   43.12 @@ -278,7 +278,7 @@
   43.13  
   43.14  fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
   43.15    Type ("fun", [@{typ Random.seed},
   43.16 -  Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
   43.17 +  Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
   43.18    | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
   43.19  
   43.20  fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
    44.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jul 01 16:54:42 2010 +0200
    44.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jul 01 16:54:44 2010 +0200
    44.3 @@ -117,7 +117,7 @@
    44.4    end;
    44.5  
    44.6  fun dest_randomT (Type ("fun", [@{typ Random.seed},
    44.7 -  Type (@{type_name "*"}, [Type (@{type_name "*"}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
    44.8 +  Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
    44.9    | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
   44.10  
   44.11  fun mk_tracing s t =
   44.12 @@ -467,7 +467,7 @@
   44.13  
   44.14  (* generation of case rules from user-given introduction rules *)
   44.15  
   44.16 -fun mk_args2 (Type (@{type_name "*"}, [T1, T2])) st =
   44.17 +fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st =
   44.18      let
   44.19        val (t1, st') = mk_args2 T1 st
   44.20        val (t2, st'') = mk_args2 T2 st'
   44.21 @@ -1099,7 +1099,7 @@
   44.22  fun all_input_of T =
   44.23    let
   44.24      val (Ts, U) = strip_type T
   44.25 -    fun input_of (Type (@{type_name "*"}, [T1, T2])) = Pair (input_of T1, input_of T2)
   44.26 +    fun input_of (Type (@{type_name Product_Type.prod}, [T1, T2])) = Pair (input_of T1, input_of T2)
   44.27        | input_of _ = Input
   44.28    in
   44.29      if U = HOLogic.boolT then
   44.30 @@ -2019,7 +2019,7 @@
   44.31    | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
   44.32    | strip_split_abs t = t
   44.33  
   44.34 -fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name "*"}, [T1, T2])) names =
   44.35 +fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
   44.36      if eq_mode (m, Input) orelse eq_mode (m, Output) then
   44.37        let
   44.38          val x = Name.variant names "x"
    45.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Thu Jul 01 16:54:42 2010 +0200
    45.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Thu Jul 01 16:54:44 2010 +0200
    45.3 @@ -36,7 +36,7 @@
    45.4  
    45.5  val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
    45.6  
    45.7 -val pair_type = (fn Type (@{type_name "*"}, _) => true | _ => false)
    45.8 +val pair_type = (fn Type (@{type_name Product_Type.prod}, _) => true | _ => false)
    45.9  val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
   45.10  
   45.11  val add_pair_rules = exists_pair_type ?? append pair_rules
    46.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Jul 01 16:54:42 2010 +0200
    46.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Jul 01 16:54:44 2010 +0200
    46.3 @@ -96,13 +96,13 @@
    46.4  (* Readable names for the more common symbolic functions. Do not mess with the
    46.5     last nine entries of the table unless you know what you are doing. *)
    46.6  val const_trans_table =
    46.7 -  Symtab.make [(@{type_name "*"}, "prod"),
    46.8 -               (@{type_name "+"}, "sum"),
    46.9 +  Symtab.make [(@{type_name Product_Type.prod}, "prod"),
   46.10 +               (@{type_name Sum_Type.sum}, "sum"),
   46.11                 (@{const_name "op ="}, "equal"),
   46.12                 (@{const_name "op &"}, "and"),
   46.13                 (@{const_name "op |"}, "or"),
   46.14                 (@{const_name "op -->"}, "implies"),
   46.15 -               (@{const_name "op :"}, "in"),
   46.16 +               (@{const_name Set.member}, "in"),
   46.17                 (@{const_name fequal}, "fequal"),
   46.18                 (@{const_name COMBI}, "COMBI"),
   46.19                 (@{const_name COMBK}, "COMBK"),
    47.1 --- a/src/HOL/Tools/TFL/rules.ML	Thu Jul 01 16:54:42 2010 +0200
    47.2 +++ b/src/HOL/Tools/TFL/rules.ML	Thu Jul 01 16:54:44 2010 +0200
    47.3 @@ -591,10 +591,10 @@
    47.4  
    47.5  local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
    47.6        fun mk_fst tm =
    47.7 -          let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm
    47.8 +          let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
    47.9            in  Const ("Product_Type.fst", ty --> fty) $ tm  end
   47.10        fun mk_snd tm =
   47.11 -          let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm
   47.12 +          let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
   47.13            in  Const ("Product_Type.snd", ty --> sty) $ tm  end
   47.14  in
   47.15  fun XFILL tych x vstruct =
    48.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Thu Jul 01 16:54:42 2010 +0200
    48.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Thu Jul 01 16:54:44 2010 +0200
    48.3 @@ -372,7 +372,7 @@
    48.4  (* Miscellaneous *)
    48.5  
    48.6  fun mk_vstruct ty V =
    48.7 -  let fun follow_prod_type (Type(@{type_name "*"},[ty1,ty2])) vs =
    48.8 +  let fun follow_prod_type (Type(@{type_name Product_Type.prod},[ty1,ty2])) vs =
    48.9                let val (ltm,vs1) = follow_prod_type ty1 vs
   48.10                    val (rtm,vs2) = follow_prod_type ty2 vs1
   48.11                in (mk_pair{fst=ltm, snd=rtm}, vs2) end
   48.12 @@ -393,7 +393,7 @@
   48.13  
   48.14  fun dest_relation tm =
   48.15     if (type_of tm = HOLogic.boolT)
   48.16 -   then let val (Const("op :",_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm
   48.17 +   then let val (Const(@{const_name Set.member},_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm
   48.18          in (R,y,x)
   48.19          end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
   48.20     else raise USYN_ERR "dest_relation" "not a boolean term";
    49.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Jul 01 16:54:42 2010 +0200
    49.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jul 01 16:54:44 2010 +0200
    49.3 @@ -173,7 +173,7 @@
    49.4                      (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
    49.5                  end
    49.6                else (case strip_type T of
    49.7 -                  (Ts, Type (@{type_name "*"}, [T1, T2])) =>
    49.8 +                  (Ts, Type (@{type_name Product_Type.prod}, [T1, T2])) =>
    49.9                      let
   49.10                        val fx = Free (x, Ts ---> T1);
   49.11                        val fr = Free (r, Ts ---> T2);
    50.1 --- a/src/HOL/Tools/split_rule.ML	Thu Jul 01 16:54:42 2010 +0200
    50.2 +++ b/src/HOL/Tools/split_rule.ML	Thu Jul 01 16:54:44 2010 +0200
    50.3 @@ -31,7 +31,7 @@
    50.4  (*In ap_split S T u, term u expects separate arguments for the factors of S,
    50.5    with result type T.  The call creates a new term expecting one argument
    50.6    of type S.*)
    50.7 -fun ap_split (Type (@{type_name "*"}, [T1, T2])) T3 u =
    50.8 +fun ap_split (Type (@{type_name Product_Type.prod}, [T1, T2])) T3 u =
    50.9        internal_split_const (T1, T2, T3) $
   50.10        Abs ("v", T1,
   50.11            ap_split T2 T3
    51.1 --- a/src/HOLCF/Bifinite.thy	Thu Jul 01 16:54:42 2010 +0200
    51.2 +++ b/src/HOLCF/Bifinite.thy	Thu Jul 01 16:54:44 2010 +0200
    51.3 @@ -161,7 +161,7 @@
    51.4      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    51.5  qed
    51.6  
    51.7 -instantiation "*" :: (profinite, profinite) profinite
    51.8 +instantiation prod :: (profinite, profinite) profinite
    51.9  begin
   51.10  
   51.11  definition
   51.12 @@ -187,7 +187,7 @@
   51.13  
   51.14  end
   51.15  
   51.16 -instance "*" :: (bifinite, bifinite) bifinite ..
   51.17 +instance prod :: (bifinite, bifinite) bifinite ..
   51.18  
   51.19  lemma approx_Pair [simp]:
   51.20    "approx i\<cdot>(x, y) = (approx i\<cdot>x, approx i\<cdot>y)"
    52.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Jul 01 16:54:42 2010 +0200
    52.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Jul 01 16:54:44 2010 +0200
    52.3 @@ -34,9 +34,9 @@
    52.4  
    52.5  exception malformed;
    52.6  
    52.7 -fun fst_type (Type(@{type_name "*"},[a,_])) = a |
    52.8 +fun fst_type (Type(@{type_name prod},[a,_])) = a |
    52.9  fst_type _ = raise malformed; 
   52.10 -fun snd_type (Type(@{type_name "*"},[_,a])) = a |
   52.11 +fun snd_type (Type(@{type_name prod},[_,a])) = a |
   52.12  snd_type _ = raise malformed;
   52.13  
   52.14  fun element_type (Type("set",[a])) = a |
   52.15 @@ -121,10 +121,10 @@
   52.16  
   52.17  fun delete_ul_string s = implode(delete_ul (explode s));
   52.18  
   52.19 -fun type_list_of sign (Type(@{type_name "*"},a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
   52.20 +fun type_list_of sign (Type(@{type_name prod},a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
   52.21  type_list_of sign a = [(Syntax.string_of_typ_global sign a)];
   52.22  
   52.23 -fun structured_tuple l (Type(@{type_name "*"},s::t::_)) =
   52.24 +fun structured_tuple l (Type(@{type_name prod},s::t::_)) =
   52.25  let
   52.26  val (r,str) = structured_tuple l s;
   52.27  in
    53.1 --- a/src/HOLCF/IOA/meta_theory/automaton.ML	Thu Jul 01 16:54:42 2010 +0200
    53.2 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Thu Jul 01 16:54:44 2010 +0200
    53.3 @@ -298,7 +298,7 @@
    53.4  (string_of_typ thy t));
    53.5  
    53.6  fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
    53.7 -comp_st_type_of thy (a::r) = Type(@{type_name "*"},[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
    53.8 +comp_st_type_of thy (a::r) = HOLogic.mk_prodT (st_type_of thy (aut_type_of thy a), comp_st_type_of thy r) |
    53.9  comp_st_type_of _ _ = error "empty automaton list";
   53.10  
   53.11  (* checking consistency of action types (for composition) *)
   53.12 @@ -378,25 +378,22 @@
   53.13  end)
   53.14  
   53.15  fun add_composition automaton_name aut_list thy =
   53.16 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   53.17 -let
   53.18 -val acttyp = check_ac thy aut_list; 
   53.19 -val st_typ = comp_st_type_of thy aut_list; 
   53.20 -val comp_list = clist aut_list;
   53.21 -in
   53.22 -thy
   53.23 -|> Sign.add_consts_i
   53.24 -[(Binding.name automaton_name,
   53.25 -Type(@{type_name "*"},
   53.26 -[Type(@{type_name "*"},[Type("set",[acttyp]),Type(@{type_name "*"},[Type("set",[acttyp]),Type("set",[acttyp])])]),
   53.27 - Type(@{type_name "*"},[Type("set",[st_typ]),
   53.28 -  Type(@{type_name "*"},[Type("set",[Type(@{type_name "*"},[st_typ,Type(@{type_name "*"},[acttyp,st_typ])])]),
   53.29 -   Type(@{type_name "*"},[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   53.30 -,NoSyn)]
   53.31 -|> add_defs
   53.32 -[(automaton_name ^ "_def",
   53.33 -automaton_name ^ " == " ^ comp_list)]
   53.34 -end)
   53.35 +  let
   53.36 +    val _ = writeln("Constructing automaton " ^ automaton_name ^ " ...")
   53.37 +    val acttyp = check_ac thy aut_list; 
   53.38 +    val st_typ = comp_st_type_of thy aut_list; 
   53.39 +    val comp_list = clist aut_list;
   53.40 +  in
   53.41 +    thy
   53.42 +    |> Sign.add_consts_i
   53.43 +        [(Binding.name automaton_name, HOLogic.mk_prodT (HOLogic.mk_prodT
   53.44 +          (HOLogic.mk_setT acttyp, HOLogic.mk_prodT (HOLogic.mk_setT acttyp, HOLogic.mk_setT acttyp)),
   53.45 +          HOLogic.mk_prodT (HOLogic.mk_setT st_typ, HOLogic.mk_prodT (HOLogic.mk_setT
   53.46 +          (HOLogic.mk_prodT (st_typ, HOLogic.mk_prodT (acttyp, st_typ))),
   53.47 +          HOLogic.mk_prodT (HOLogic.mk_setT (HOLogic.mk_setT acttyp), HOLogic.mk_setT (HOLogic.mk_setT acttyp))))),
   53.48 +            NoSyn)]
   53.49 +    |> add_defs [(automaton_name ^ "_def", automaton_name ^ " == " ^ comp_list)]
   53.50 +  end
   53.51  
   53.52  fun add_restriction automaton_name aut_source actlist thy =
   53.53  (writeln("Constructing automaton " ^ automaton_name ^ " ...");
   53.54 @@ -433,25 +430,23 @@
   53.55    | _ => error "could not extract argument type of renaming function term");
   53.56   
   53.57  fun add_rename automaton_name aut_source fun_name thy =
   53.58 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   53.59 -let
   53.60 -val auttyp = aut_type_of thy aut_source;
   53.61 -val st_typ = st_type_of thy auttyp;
   53.62 -val acttyp = ren_act_type_of thy fun_name
   53.63 -in
   53.64 -thy
   53.65 -|> Sign.add_consts_i
   53.66 -[(Binding.name automaton_name,
   53.67 -Type(@{type_name "*"},
   53.68 -[Type(@{type_name "*"},[Type("set",[acttyp]),Type(@{type_name "*"},[Type("set",[acttyp]),Type("set",[acttyp])])]),
   53.69 - Type(@{type_name "*"},[Type("set",[st_typ]),
   53.70 -  Type(@{type_name "*"},[Type("set",[Type(@{type_name "*"},[st_typ,Type(@{type_name "*"},[acttyp,st_typ])])]),
   53.71 -   Type(@{type_name "*"},[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   53.72 -,NoSyn)]
   53.73 -|> add_defs
   53.74 -[(automaton_name ^ "_def",
   53.75 -automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
   53.76 -end)
   53.77 +  let
   53.78 +    val _ = writeln("Constructing automaton " ^ automaton_name ^ " ...")
   53.79 +    val auttyp = aut_type_of thy aut_source;
   53.80 +    val st_typ = st_type_of thy auttyp;
   53.81 +    val acttyp = ren_act_type_of thy fun_name
   53.82 +  in
   53.83 +    thy
   53.84 +    |> Sign.add_consts_i
   53.85 +        [(Binding.name automaton_name,
   53.86 +        Type(@{type_name prod},
   53.87 +        [Type(@{type_name prod},[HOLogic.mk_setT acttyp,Type(@{type_name prod},[HOLogic.mk_setT acttyp,HOLogic.mk_setT acttyp])]),
   53.88 +         Type(@{type_name prod},[HOLogic.mk_setT st_typ,
   53.89 +          Type(@{type_name prod},[HOLogic.mk_setT (Type(@{type_name prod},[st_typ,Type(@{type_name prod},[acttyp,st_typ])])),
   53.90 +           Type(@{type_name prod},[HOLogic.mk_setT (HOLogic.mk_setT acttyp),HOLogic.mk_setT (HOLogic.mk_setT acttyp)])])])])
   53.91 +        ,NoSyn)]
   53.92 +    |> add_defs [(automaton_name ^ "_def", automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
   53.93 +  end
   53.94  
   53.95  
   53.96  (** outer syntax **)
    54.1 --- a/src/HOLCF/Library/Sum_Cpo.thy	Thu Jul 01 16:54:42 2010 +0200
    54.2 +++ b/src/HOLCF/Library/Sum_Cpo.thy	Thu Jul 01 16:54:44 2010 +0200
    54.3 @@ -10,7 +10,7 @@
    54.4  
    54.5  subsection {* Ordering on sum type *}
    54.6  
    54.7 -instantiation "+" :: (below, below) below
    54.8 +instantiation sum :: (below, below) below
    54.9  begin
   54.10  
   54.11  definition below_sum_def:
   54.12 @@ -56,7 +56,7 @@
   54.13  
   54.14  subsection {* Sum type is a complete partial order *}
   54.15  
   54.16 -instance "+" :: (po, po) po
   54.17 +instance sum :: (po, po) po
   54.18  proof
   54.19    fix x :: "'a + 'b"
   54.20    show "x \<sqsubseteq> x"
   54.21 @@ -117,7 +117,7 @@
   54.22   apply (drule ub_rangeD, simp)
   54.23  done
   54.24  
   54.25 -instance "+" :: (cpo, cpo) cpo
   54.26 +instance sum :: (cpo, cpo) cpo
   54.27   apply intro_classes
   54.28   apply (erule sum_chain_cases, safe)
   54.29    apply (rule exI)
   54.30 @@ -217,20 +217,20 @@
   54.31  lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a"
   54.32  by (safe elim!: compact_Inr compact_Inr_rev)
   54.33  
   54.34 -instance "+" :: (chfin, chfin) chfin
   54.35 +instance sum :: (chfin, chfin) chfin
   54.36  apply intro_classes
   54.37  apply (erule compact_imp_max_in_chain)
   54.38  apply (case_tac "\<Squnion>i. Y i", simp_all)
   54.39  done
   54.40  
   54.41 -instance "+" :: (finite_po, finite_po) finite_po ..
   54.42 +instance sum :: (finite_po, finite_po) finite_po ..
   54.43  
   54.44 -instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
   54.45 +instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo
   54.46  by intro_classes (simp add: below_sum_def split: sum.split)
   54.47  
   54.48  subsection {* Sum type is a bifinite domain *}
   54.49  
   54.50 -instantiation "+" :: (profinite, profinite) profinite
   54.51 +instantiation sum :: (profinite, profinite) profinite
   54.52  begin
   54.53  
   54.54  definition
    55.1 --- a/src/HOLCF/Product_Cpo.thy	Thu Jul 01 16:54:42 2010 +0200
    55.2 +++ b/src/HOLCF/Product_Cpo.thy	Thu Jul 01 16:54:44 2010 +0200
    55.3 @@ -32,7 +32,7 @@
    55.4  
    55.5  subsection {* Product type is a partial order *}
    55.6  
    55.7 -instantiation "*" :: (below, below) below
    55.8 +instantiation prod :: (below, below) below
    55.9  begin
   55.10  
   55.11  definition
   55.12 @@ -41,7 +41,7 @@
   55.13  instance ..
   55.14  end
   55.15  
   55.16 -instance "*" :: (po, po) po
   55.17 +instance prod :: (po, po) po
   55.18  proof
   55.19    fix x :: "'a \<times> 'b"
   55.20    show "x \<sqsubseteq> x"
   55.21 @@ -148,7 +148,7 @@
   55.22      \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   55.23  by (rule lub_cprod [THEN thelubI])
   55.24  
   55.25 -instance "*" :: (cpo, cpo) cpo
   55.26 +instance prod :: (cpo, cpo) cpo
   55.27  proof
   55.28    fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
   55.29    assume "chain S"
   55.30 @@ -157,9 +157,9 @@
   55.31    thus "\<exists>x. range S <<| x" ..
   55.32  qed
   55.33  
   55.34 -instance "*" :: (finite_po, finite_po) finite_po ..
   55.35 +instance prod :: (finite_po, finite_po) finite_po ..
   55.36  
   55.37 -instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo
   55.38 +instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
   55.39  proof
   55.40    fix x y :: "'a \<times> 'b"
   55.41    show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
   55.42 @@ -172,7 +172,7 @@
   55.43  lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
   55.44  by (simp add: below_prod_def)
   55.45  
   55.46 -instance "*" :: (pcpo, pcpo) pcpo
   55.47 +instance prod :: (pcpo, pcpo) pcpo
   55.48  by intro_classes (fast intro: minimal_cprod)
   55.49  
   55.50  lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
   55.51 @@ -297,7 +297,7 @@
   55.52  apply (drule compact_snd, simp)
   55.53  done
   55.54  
   55.55 -instance "*" :: (chfin, chfin) chfin
   55.56 +instance prod :: (chfin, chfin) chfin
   55.57  apply intro_classes
   55.58  apply (erule compact_imp_max_in_chain)
   55.59  apply (case_tac "\<Squnion>i. Y i", simp)
    56.1 --- a/src/HOLCF/Representable.thy	Thu Jul 01 16:54:42 2010 +0200
    56.2 +++ b/src/HOLCF/Representable.thy	Thu Jul 01 16:54:44 2010 +0200
    56.3 @@ -447,7 +447,7 @@
    56.4  
    56.5  text "Cartesian products of representable types are representable."
    56.6  
    56.7 -instantiation "*" :: (rep, rep) rep
    56.8 +instantiation prod :: (rep, rep) rep
    56.9  begin
   56.10  
   56.11  definition emb_cprod_def: "emb = udom_emb oo cprod_map\<cdot>emb\<cdot>emb"
   56.12 @@ -763,7 +763,7 @@
   56.13       (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
   56.14          @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
   56.15  
   56.16 -     (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
   56.17 +     (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
   56.18          @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
   56.19  
   56.20       (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm REP_up},
    57.1 --- a/src/Pure/Isar/class_target.ML	Thu Jul 01 16:54:42 2010 +0200
    57.2 +++ b/src/Pure/Isar/class_target.ML	Thu Jul 01 16:54:44 2010 +0200
    57.3 @@ -450,7 +450,7 @@
    57.4  
    57.5  (* target *)
    57.6  
    57.7 -val sanitize_name = (*FIXME*)
    57.8 +val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*)
    57.9    let
   57.10      fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
   57.11        orelse s = "'" orelse s = "_";
   57.12 @@ -465,9 +465,7 @@
   57.13      explode #> scan_valids #> implode
   57.14    end;
   57.15  
   57.16 -fun type_name "Product_Type.*" = "prod"
   57.17 -  | type_name "Sum_Type.+" = "sum"
   57.18 -  | type_name s = sanitize_name (Long_Name.base_name s);
   57.19 +val type_name = sanitize_name o Long_Name.base_name;
   57.20  
   57.21  fun resort_terms pp algebra consts constraints ts =
   57.22    let