--- a/src/HOL/Real/Rational.thy Fri Aug 31 23:17:25 2007 +0200
+++ b/src/HOL/Real/Rational.thy Sat Sep 01 01:21:48 2007 +0200
@@ -209,6 +209,9 @@
instance rat :: abs
abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)" ..
+instance rat :: sgn
+ sgn_rat_def: "sgn(q::rat) == (if q=0 then 0 else if 0<q then 1 else - 1)" ..
+
instance rat :: power ..
primrec (rat)
@@ -405,7 +408,7 @@
qed
show "\<bar>q\<bar> = (if q < 0 then -q else q)"
by (simp only: abs_rat_def)
-qed auto
+qed (auto simp: sgn_rat_def)
instance rat :: division_by_zero
proof