denominator should not be zero
authorhaftmann
Tue Jun 16 16:26:40 2009 +0200 (2009-06-16)
changeset 31666760c612ad800
parent 31665 a1f4d3b3f6c8
child 31667 cc969090c204
denominator should not be zero
src/HOL/Rational.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Rational.thy	Tue Jun 16 14:56:59 2009 +0200
     1.2 +++ b/src/HOL/Rational.thy	Tue Jun 16 16:26:40 2009 +0200
     1.3 @@ -1048,7 +1048,7 @@
     1.4      val p' = p div g;
     1.5      val q' = q div g;
     1.6      val r = (if one_of [true, false] then p' else ~ p',
     1.7 -      if p' = 0 then 0 else q')
     1.8 +      if p' = 0 then 1 else q')
     1.9    in
    1.10      (r, fn () => term_of_rat r)
    1.11    end;
    1.12 @@ -1060,8 +1060,7 @@
    1.13  consts_code
    1.14    "of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int")
    1.15  attach {*
    1.16 -fun rat_of_int 0 = (0, 0)
    1.17 -  | rat_of_int i = (i, 1);
    1.18 +fun rat_of_int i (i, 1);
    1.19  *}
    1.20  
    1.21  end
     2.1 --- a/src/HOL/RealDef.thy	Tue Jun 16 14:56:59 2009 +0200
     2.2 +++ b/src/HOL/RealDef.thy	Tue Jun 16 16:26:40 2009 +0200
     2.3 @@ -1169,7 +1169,7 @@
     2.4      val p' = p div g;
     2.5      val q' = q div g;
     2.6      val r = (if one_of [true, false] then p' else ~ p',
     2.7 -      if p' = 0 then 0 else q')
     2.8 +      if p' = 0 then 1 else q')
     2.9    in
    2.10      (r, fn () => term_of_real r)
    2.11    end;
    2.12 @@ -1181,8 +1181,7 @@
    2.13  consts_code
    2.14    "of_int :: int \<Rightarrow> real" ("\<module>real'_of'_int")
    2.15  attach {*
    2.16 -fun real_of_int 0 = (0, 0)
    2.17 -  | real_of_int i = (i, 1);
    2.18 +fun real_of_int i = (i, 1);
    2.19  *}
    2.20  
    2.21  end