src/HOL/Rational.thy
 changeset 29332 edc1e2a56398 parent 28952 15a4b2cf8c34 child 29667 53103fc8ffa3
```     1.1 --- a/src/HOL/Rational.thy	Tue Dec 30 11:10:01 2008 +0100
1.2 +++ b/src/HOL/Rational.thy	Fri Jan 02 08:12:46 2009 +0100
1.3 @@ -851,7 +851,7 @@
1.4  definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where
1.5    [simp, code del]: "Fract_norm a b = Fract a b"
1.6
1.7 -lemma [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
1.8 +lemma Fract_norm_code [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
1.9    if b > 0 then Fract (a div c) (b div c) else Fract (- (a div c)) (- (b div c)))"
1.10    by (simp add: eq_rat Zero_rat_def Let_def Fract_norm)
1.11
1.12 @@ -871,7 +871,7 @@
1.13         then c = 0 \<or> d = 0
1.14       else if d = 0
1.15         then a = 0 \<or> b = 0
1.16 -     else a * d =  b * c)"
1.17 +     else a * d = b * c)"
1.18    by (auto simp add: eq eq_rat)
1.19
1.20  lemma rat_eq_refl [code nbe]:
```