# HG changeset patch # User haftmann # Date 1230880366 -3600 # Node ID edc1e2a563988e2f1e3d481bce805bfca926cef8 # Parent ea97aa6aeba2b790c69d6a3b1ba1e6913a3519ca named code theorem for Fract_norm diff -r ea97aa6aeba2 -r edc1e2a56398 src/HOL/Rational.thy --- a/src/HOL/Rational.thy Tue Dec 30 11:10:01 2008 +0100 +++ b/src/HOL/Rational.thy Fri Jan 02 08:12:46 2009 +0100 @@ -851,7 +851,7 @@ definition Fract_norm :: "int \ int \ rat" where [simp, code del]: "Fract_norm a b = Fract a b" -lemma [code]: "Fract_norm a b = (if a = 0 \ b = 0 then 0 else let c = zgcd a b in +lemma Fract_norm_code [code]: "Fract_norm a b = (if a = 0 \ b = 0 then 0 else let c = zgcd a b in if b > 0 then Fract (a div c) (b div c) else Fract (- (a div c)) (- (b div c)))" by (simp add: eq_rat Zero_rat_def Let_def Fract_norm) @@ -871,7 +871,7 @@ then c = 0 \ d = 0 else if d = 0 then a = 0 \ b = 0 - else a * d = b * c)" + else a * d = b * c)" by (auto simp add: eq eq_rat) lemma rat_eq_refl [code nbe]: