src/HOL/Real/RealDef.thy
changeset 24630 351a308ab58d
parent 24623 7b2bc73405b8
child 25112 98824cc791c0
     1.1 --- a/src/HOL/Real/RealDef.thy	Tue Sep 18 11:06:22 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Tue Sep 18 16:08:00 2007 +0200
     1.3 @@ -1011,8 +1011,8 @@
     1.4      val p = random_range 0 i;
     1.5      val q = random_range 1 (i + 1);
     1.6      val g = Integer.gcd p q;
     1.7 -    val p' = Integer.div p g;
     1.8 -    val q' = Integer.div q g;
     1.9 +    val p' = p div g;
    1.10 +    val q' = q div g;
    1.11    in
    1.12      (if one_of [true, false] then p' else ~ p',
    1.13       if p' = 0 then 0 else q')