src/HOL/Rat.thy
changeset 39910 10097e0a9dbd
parent 38857 97775f3e8722
child 40815 6e2d17cc0d1d
     1.1 --- a/src/HOL/Rat.thy	Fri Oct 01 14:15:49 2010 +0200
     1.2 +++ b/src/HOL/Rat.thy	Fri Oct 01 16:05:25 2010 +0200
     1.3 @@ -470,7 +470,7 @@
     1.4  
     1.5  definition
     1.6    le_rat_def:
     1.7 -   "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
     1.8 +   "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
     1.9        {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})"
    1.10  
    1.11  lemma le_rat [simp]:
    1.12 @@ -775,7 +775,7 @@
    1.13  begin
    1.14  
    1.15  definition of_rat :: "rat \<Rightarrow> 'a" where
    1.16 -  "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
    1.17 +  "of_rat q = the_elem (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
    1.18  
    1.19  end
    1.20