constant `contents` renamed to `the_elem`
authorhaftmann
Fri Oct 01 16:05:25 2010 +0200 (2010-10-01 ago)
changeset 3991010097e0a9dbd
parent 39818 ff9e9d5ac171
child 39911 2b4430847310
constant `contents` renamed to `the_elem`
NEWS
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Coset.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Int.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Rat.thy
src/HOL/Set.thy
src/HOL/Word/Misc_Numeric.thy
src/HOL/Word/Word.thy
src/HOL/ZF/Games.thy
src/HOL/ex/Dedekind_Real.thy
     1.1 --- a/NEWS	Fri Oct 01 14:15:49 2010 +0200
     1.2 +++ b/NEWS	Fri Oct 01 16:05:25 2010 +0200
     1.3 @@ -74,6 +74,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Constant `contents` renamed to `the_elem`, to free the generic name
     1.8 +contents for other uses.  INCOMPATIBILITY.
     1.9 +
    1.10  * Dropped old primrec package.  INCOMPATIBILITY.
    1.11  
    1.12  * Improved infrastructure for term evaluation using code generator
     2.1 --- a/src/HOL/Algebra/AbelCoset.thy	Fri Oct 01 14:15:49 2010 +0200
     2.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Fri Oct 01 16:05:25 2010 +0200
     2.3 @@ -607,20 +607,20 @@
     2.4  by (rule group_hom.FactGroup_nonempty[OF a_group_hom,
     2.5      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
     2.6  
     2.7 -lemma (in abelian_group_hom) FactGroup_contents_mem:
     2.8 +lemma (in abelian_group_hom) FactGroup_the_elem_mem:
     2.9    assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))"
    2.10 -  shows "contents (h`X) \<in> carrier H"
    2.11 -by (rule group_hom.FactGroup_contents_mem[OF a_group_hom,
    2.12 +  shows "the_elem (h`X) \<in> carrier H"
    2.13 +by (rule group_hom.FactGroup_the_elem_mem[OF a_group_hom,
    2.14      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
    2.15  
    2.16  lemma (in abelian_group_hom) A_FactGroup_hom:
    2.17 -     "(\<lambda>X. contents (h`X)) \<in> hom (G A_Mod (a_kernel G H h))
    2.18 +     "(\<lambda>X. the_elem (h`X)) \<in> hom (G A_Mod (a_kernel G H h))
    2.19            \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr>"
    2.20  by (rule group_hom.FactGroup_hom[OF a_group_hom,
    2.21      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
    2.22  
    2.23  lemma (in abelian_group_hom) A_FactGroup_inj_on:
    2.24 -     "inj_on (\<lambda>X. contents (h ` X)) (carrier (G A_Mod a_kernel G H h))"
    2.25 +     "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G A_Mod a_kernel G H h))"
    2.26  by (rule group_hom.FactGroup_inj_on[OF a_group_hom,
    2.27      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
    2.28  
    2.29 @@ -628,7 +628,7 @@
    2.30  homomorphism from the quotient group*}
    2.31  lemma (in abelian_group_hom) A_FactGroup_onto:
    2.32    assumes h: "h ` carrier G = carrier H"
    2.33 -  shows "(\<lambda>X. contents (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
    2.34 +  shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
    2.35  by (rule group_hom.FactGroup_onto[OF a_group_hom,
    2.36      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)
    2.37  
    2.38 @@ -636,7 +636,7 @@
    2.39   quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
    2.40  theorem (in abelian_group_hom) A_FactGroup_iso:
    2.41    "h ` carrier G = carrier H
    2.42 -   \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
    2.43 +   \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
    2.44            (| carrier = carrier H, mult = add H, one = zero H |)"
    2.45  by (rule group_hom.FactGroup_iso[OF a_group_hom,
    2.46      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
     3.1 --- a/src/HOL/Algebra/Coset.thy	Fri Oct 01 14:15:49 2010 +0200
     3.2 +++ b/src/HOL/Algebra/Coset.thy	Fri Oct 01 16:05:25 2010 +0200
     3.3 @@ -924,9 +924,9 @@
     3.4  qed
     3.5  
     3.6  
     3.7 -lemma (in group_hom) FactGroup_contents_mem:
     3.8 +lemma (in group_hom) FactGroup_the_elem_mem:
     3.9    assumes X: "X \<in> carrier (G Mod (kernel G H h))"
    3.10 -  shows "contents (h`X) \<in> carrier H"
    3.11 +  shows "the_elem (h`X) \<in> carrier H"
    3.12  proof -
    3.13    from X
    3.14    obtain g where g: "g \<in> carrier G" 
    3.15 @@ -937,8 +937,8 @@
    3.16  qed
    3.17  
    3.18  lemma (in group_hom) FactGroup_hom:
    3.19 -     "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
    3.20 -apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
    3.21 +     "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
    3.22 +apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
    3.23  proof (intro ballI)
    3.24    fix X and X'
    3.25    assume X:  "X  \<in> carrier (G Mod kernel G H h)"
    3.26 @@ -955,7 +955,7 @@
    3.27      by (auto dest!: FactGroup_nonempty
    3.28               simp add: set_mult_def image_eq_UN 
    3.29                         subsetD [OF Xsub] subsetD [OF X'sub]) 
    3.30 -  thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
    3.31 +  thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
    3.32      by (simp add: all image_eq_UN FactGroup_nonempty X X')
    3.33  qed
    3.34  
    3.35 @@ -971,7 +971,7 @@
    3.36  done
    3.37  
    3.38  lemma (in group_hom) FactGroup_inj_on:
    3.39 -     "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
    3.40 +     "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
    3.41  proof (simp add: inj_on_def, clarify) 
    3.42    fix X and X'
    3.43    assume X:  "X  \<in> carrier (G Mod kernel G H h)"
    3.44 @@ -983,7 +983,7 @@
    3.45      by (auto simp add: FactGroup_def RCOSETS_def)
    3.46    hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
    3.47      by (force simp add: kernel_def r_coset_def image_def)+
    3.48 -  assume "contents (h ` X) = contents (h ` X')"
    3.49 +  assume "the_elem (h ` X) = the_elem (h ` X')"
    3.50    hence h: "h g = h g'"
    3.51      by (simp add: image_eq_UN all FactGroup_nonempty X X') 
    3.52    show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
    3.53 @@ -993,11 +993,11 @@
    3.54  homomorphism from the quotient group*}
    3.55  lemma (in group_hom) FactGroup_onto:
    3.56    assumes h: "h ` carrier G = carrier H"
    3.57 -  shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
    3.58 +  shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
    3.59  proof
    3.60 -  show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
    3.61 -    by (auto simp add: FactGroup_contents_mem)
    3.62 -  show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
    3.63 +  show "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
    3.64 +    by (auto simp add: FactGroup_the_elem_mem)
    3.65 +  show "carrier H \<subseteq> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
    3.66    proof
    3.67      fix y
    3.68      assume y: "y \<in> carrier H"
    3.69 @@ -1005,7 +1005,7 @@
    3.70        by (blast elim: equalityE) 
    3.71      hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
    3.72        by (auto simp add: y kernel_def r_coset_def) 
    3.73 -    with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 
    3.74 +    with g show "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)" 
    3.75        by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
    3.76    qed
    3.77  qed
    3.78 @@ -1015,7 +1015,7 @@
    3.79   quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
    3.80  theorem (in group_hom) FactGroup_iso:
    3.81    "h ` carrier G = carrier H
    3.82 -   \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
    3.83 +   \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
    3.84  by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
    3.85                FactGroup_onto) 
    3.86  
     4.1 --- a/src/HOL/Induct/QuoDataType.thy	Fri Oct 01 14:15:49 2010 +0200
     4.2 +++ b/src/HOL/Induct/QuoDataType.thy	Fri Oct 01 16:05:25 2010 +0200
     4.3 @@ -422,7 +422,7 @@
     4.4  
     4.5  definition
     4.6    discrim :: "msg \<Rightarrow> int" where
     4.7 -   "discrim X = contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
     4.8 +   "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
     4.9  
    4.10  lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
    4.11  by (simp add: congruent_def msgrel_imp_eq_freediscrim) 
     5.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Fri Oct 01 14:15:49 2010 +0200
     5.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Fri Oct 01 16:05:25 2010 +0200
     5.3 @@ -337,7 +337,7 @@
     5.4  
     5.5  definition
     5.6    "fun" :: "exp \<Rightarrow> nat" where
     5.7 -  "fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
     5.8 +  "fun X = the_elem (\<Union>U \<in> Rep_Exp X. {freefun U})"
     5.9  
    5.10  lemma fun_respects: "(%U. {freefun U}) respects exprel"
    5.11  by (simp add: congruent_def exprel_imp_eq_freefun) 
    5.12 @@ -349,7 +349,7 @@
    5.13  
    5.14  definition
    5.15    args :: "exp \<Rightarrow> exp list" where
    5.16 -  "args X = contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
    5.17 +  "args X = the_elem (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
    5.18  
    5.19  text{*This result can probably be generalized to arbitrary equivalence
    5.20  relations, but with little benefit here.*}
    5.21 @@ -384,7 +384,7 @@
    5.22  
    5.23  definition
    5.24    discrim :: "exp \<Rightarrow> int" where
    5.25 -  "discrim X = contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
    5.26 +  "discrim X = the_elem (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
    5.27  
    5.28  lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
    5.29  by (simp add: congruent_def exprel_imp_eq_freediscrim) 
     6.1 --- a/src/HOL/Int.thy	Fri Oct 01 14:15:49 2010 +0200
     6.2 +++ b/src/HOL/Int.thy	Fri Oct 01 16:05:25 2010 +0200
     6.3 @@ -283,7 +283,7 @@
     6.4  begin
     6.5  
     6.6  definition of_int :: "int \<Rightarrow> 'a" where
     6.7 -  "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
     6.8 +  "of_int z = the_elem (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
     6.9  
    6.10  lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
    6.11  proof -
    6.12 @@ -389,7 +389,7 @@
    6.13  subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
    6.14  
    6.15  definition nat :: "int \<Rightarrow> nat" where
    6.16 -  "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
    6.17 +  "nat z = the_elem (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
    6.18  
    6.19  lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
    6.20  proof -
     7.1 --- a/src/HOL/Library/Fraction_Field.thy	Fri Oct 01 14:15:49 2010 +0200
     7.2 +++ b/src/HOL/Library/Fraction_Field.thy	Fri Oct 01 16:05:25 2010 +0200
     7.3 @@ -319,7 +319,7 @@
     7.4  
     7.5  definition
     7.6    le_fract_def:
     7.7 -   "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
     7.8 +   "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
     7.9        {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
    7.10  
    7.11  definition
     8.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Oct 01 14:15:49 2010 +0200
     8.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Oct 01 16:05:25 2010 +0200
     8.3 @@ -495,7 +495,7 @@
     8.4  
     8.5  lemma (in measure_space) simple_function_partition:
     8.6    assumes "simple_function f" and "simple_function g"
     8.7 -  shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. contents (f`A) * \<mu> A)"
     8.8 +  shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. the_elem (f`A) * \<mu> A)"
     8.9      (is "_ = setsum _ (?p ` space M)")
    8.10  proof-
    8.11    let "?sub x" = "?p ` (f -` {x} \<inter> space M)"
    8.12 @@ -530,18 +530,18 @@
    8.13      unfolding simple_integral_def
    8.14      by (subst setsum_Sigma[symmetric],
    8.15         auto intro!: setsum_cong simp: setsum_right_distrib[symmetric])
    8.16 -  also have "\<dots> = (\<Sum>A\<in>?p ` space M. contents (f`A) * \<mu> A)"
    8.17 +  also have "\<dots> = (\<Sum>A\<in>?p ` space M. the_elem (f`A) * \<mu> A)"
    8.18    proof -
    8.19      have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI)
    8.20 -    have "(\<lambda>A. (contents (f ` A), A)) ` ?p ` space M
    8.21 +    have "(\<lambda>A. (the_elem (f ` A), A)) ` ?p ` space M
    8.22        = (\<lambda>x. (f x, ?p x)) ` space M"
    8.23      proof safe
    8.24        fix x assume "x \<in> space M"
    8.25 -      thus "(f x, ?p x) \<in> (\<lambda>A. (contents (f`A), A)) ` ?p ` space M"
    8.26 +      thus "(f x, ?p x) \<in> (\<lambda>A. (the_elem (f`A), A)) ` ?p ` space M"
    8.27          by (auto intro!: image_eqI[of _ _ "?p x"])
    8.28      qed auto
    8.29      thus ?thesis
    8.30 -      apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (contents (f`A), A)"] inj_onI)
    8.31 +      apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (the_elem (f`A), A)"] inj_onI)
    8.32        apply (rule_tac x="xa" in image_eqI)
    8.33        by simp_all
    8.34    qed
    8.35 @@ -602,7 +602,7 @@
    8.36    fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
    8.37    assume "x \<in> space M"
    8.38    hence "f ` ?S = {f x}" "g ` ?S = {g x}" by auto
    8.39 -  thus "contents (f`?S) * \<mu> ?S \<le> contents (g`?S) * \<mu> ?S"
    8.40 +  thus "the_elem (f`?S) * \<mu> ?S \<le> the_elem (g`?S) * \<mu> ?S"
    8.41      using mono[OF `x \<in> space M`] by (auto intro!: mult_right_mono)
    8.42  qed
    8.43  
     9.1 --- a/src/HOL/Rat.thy	Fri Oct 01 14:15:49 2010 +0200
     9.2 +++ b/src/HOL/Rat.thy	Fri Oct 01 16:05:25 2010 +0200
     9.3 @@ -470,7 +470,7 @@
     9.4  
     9.5  definition
     9.6    le_rat_def:
     9.7 -   "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
     9.8 +   "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
     9.9        {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})"
    9.10  
    9.11  lemma le_rat [simp]:
    9.12 @@ -775,7 +775,7 @@
    9.13  begin
    9.14  
    9.15  definition of_rat :: "rat \<Rightarrow> 'a" where
    9.16 -  "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
    9.17 +  "of_rat q = the_elem (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
    9.18  
    9.19  end
    9.20  
    10.1 --- a/src/HOL/Set.thy	Fri Oct 01 14:15:49 2010 +0200
    10.2 +++ b/src/HOL/Set.thy	Fri Oct 01 16:05:25 2010 +0200
    10.3 @@ -1656,11 +1656,11 @@
    10.4  
    10.5  subsubsection {* Getting the Contents of a Singleton Set *}
    10.6  
    10.7 -definition contents :: "'a set \<Rightarrow> 'a" where
    10.8 -  "contents X = (THE x. X = {x})"
    10.9 +definition the_elem :: "'a set \<Rightarrow> 'a" where
   10.10 +  "the_elem X = (THE x. X = {x})"
   10.11  
   10.12 -lemma contents_eq [simp]: "contents {x} = x"
   10.13 -  by (simp add: contents_def)
   10.14 +lemma the_elem_eq [simp]: "the_elem {x} = x"
   10.15 +  by (simp add: the_elem_def)
   10.16  
   10.17  
   10.18  subsubsection {* Least value operator *}
    11.1 --- a/src/HOL/Word/Misc_Numeric.thy	Fri Oct 01 14:15:49 2010 +0200
    11.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Fri Oct 01 16:05:25 2010 +0200
    11.3 @@ -8,8 +8,8 @@
    11.4  imports Main Parity
    11.5  begin
    11.6  
    11.7 -lemma contentsI: "y = {x} ==> contents y = x" 
    11.8 -  unfolding contents_def by auto -- {* FIXME move *}
    11.9 +lemma the_elemI: "y = {x} ==> the_elem y = x" 
   11.10 +  by simp
   11.11  
   11.12  lemmas split_split = prod.split
   11.13  lemmas split_split_asm = prod.split_asm
    12.1 --- a/src/HOL/Word/Word.thy	Fri Oct 01 14:15:49 2010 +0200
    12.2 +++ b/src/HOL/Word/Word.thy	Fri Oct 01 16:05:25 2010 +0200
    12.3 @@ -1772,7 +1772,7 @@
    12.4  lemma word_of_int: "of_int = word_of_int"
    12.5    apply (rule ext)
    12.6    apply (unfold of_int_def)
    12.7 -  apply (rule contentsI)
    12.8 +  apply (rule the_elemI)
    12.9    apply safe
   12.10    apply (simp_all add: word_of_nat word_of_int_homs)
   12.11     defer
    13.1 --- a/src/HOL/ZF/Games.thy	Fri Oct 01 14:15:49 2010 +0200
    13.2 +++ b/src/HOL/ZF/Games.thy	Fri Oct 01 16:05:25 2010 +0200
    13.3 @@ -859,10 +859,10 @@
    13.4    Pg_less_def: "G < H \<longleftrightarrow> G \<le> H \<and> G \<noteq> (H::Pg)"
    13.5  
    13.6  definition
    13.7 -  Pg_minus_def: "- G = contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
    13.8 +  Pg_minus_def: "- G = the_elem (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
    13.9  
   13.10  definition
   13.11 -  Pg_plus_def: "G + H = contents (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
   13.12 +  Pg_plus_def: "G + H = the_elem (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
   13.13  
   13.14  definition
   13.15    Pg_diff_def: "G - H = G + (- (H::Pg))"
    14.1 --- a/src/HOL/ex/Dedekind_Real.thy	Fri Oct 01 14:15:49 2010 +0200
    14.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Fri Oct 01 16:05:25 2010 +0200
    14.3 @@ -1183,11 +1183,11 @@
    14.4  
    14.5  definition
    14.6    real_add_def: "z + w =
    14.7 -       contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    14.8 +       the_elem (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    14.9                   { Abs_Real(realrel``{(x+u, y+v)}) })"
   14.10  
   14.11  definition
   14.12 -  real_minus_def: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
   14.13 +  real_minus_def: "- r =  the_elem (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
   14.14  
   14.15  definition
   14.16    real_diff_def: "r - (s::real) = r + - s"
   14.17 @@ -1195,7 +1195,7 @@
   14.18  definition
   14.19    real_mult_def:
   14.20      "z * w =
   14.21 -       contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
   14.22 +       the_elem (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
   14.23                   { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
   14.24  
   14.25  definition