--- a/src/HOL/Real/Rational.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/Rational.thy Wed Jan 02 15:14:02 2008 +0100
@@ -6,7 +6,7 @@
header {* Rational numbers *}
theory Rational
-imports Abstract_Rat
+imports "~~/src/HOL/Library/Abstract_Rat"
uses ("rat_arith.ML")
begin
@@ -163,7 +163,7 @@
subsubsection {* Standard operations on rational numbers *}
-instantiation rat :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
+instantiation rat :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
begin
definition