src/HOL/Library/Fraction_Field.thy
changeset 39910 10097e0a9dbd
parent 37765 26bdfb7b680b
child 40815 6e2d17cc0d1d
     1.1 --- a/src/HOL/Library/Fraction_Field.thy	Fri Oct 01 14:15:49 2010 +0200
     1.2 +++ b/src/HOL/Library/Fraction_Field.thy	Fri Oct 01 16:05:25 2010 +0200
     1.3 @@ -319,7 +319,7 @@
     1.4  
     1.5  definition
     1.6    le_fract_def:
     1.7 -   "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
     1.8 +   "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
     1.9        {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
    1.10  
    1.11  definition