src/HOL/Int.thy
changeset 39910 10097e0a9dbd
parent 38857 97775f3e8722
child 40819 2ac5af6eb8a8
     1.1 --- a/src/HOL/Int.thy	Fri Oct 01 14:15:49 2010 +0200
     1.2 +++ b/src/HOL/Int.thy	Fri Oct 01 16:05:25 2010 +0200
     1.3 @@ -283,7 +283,7 @@
     1.4  begin
     1.5  
     1.6  definition of_int :: "int \<Rightarrow> 'a" where
     1.7 -  "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
     1.8 +  "of_int z = the_elem (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
     1.9  
    1.10  lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
    1.11  proof -
    1.12 @@ -389,7 +389,7 @@
    1.13  subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
    1.14  
    1.15  definition nat :: "int \<Rightarrow> nat" where
    1.16 -  "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
    1.17 +  "nat z = the_elem (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
    1.18  
    1.19  lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
    1.20  proof -